<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8"/>
<link href="common/css/sf.css" rel="stylesheet" type="text/css"/>
<title>QC: Core QuickChick</title>
</head>
<link href="common/jquery-ui/jquery-ui.css" rel="stylesheet">
<script src="common/jquery-ui/external/jquery/jquery.js"></script>
<script src="common/jquery-ui/jquery-ui.js"></script>
<script src="common/toggleproofs.js"></script>
<link href="common/css/qc.css" rel="stylesheet" type="text/css"/>

<body>

<div id="page">

<div id="header">
<a href='https://coq-zh.github.io/SF-zh/index.html'>
<img src='common/media/image/sf_logo_sm.png'></a>
</br><a href='index.html'>  <span class='booktitleinheader'>Volume 4: QuickChick：用 Coq 进行基于性质的测试</span><br></br>
<ul id='menu'>
   <a href='toc.html'><li class='section_name'>目录</li></a>
   <a href='coqindex.html'><li class='section_name'>索引</li></a>
</ul>
</a></div>

<div id="main">

<h1 class="libtitle">QC<span class="subtitle">Core QuickChick</span></h1>



<div class="doc">
<a name="lab50"></a><h1 class="section">Generators</h1>

<div class="paragraph"> </div>

 The heart of property-based random testing is generation of random
    inputs.  
</div>

<div class="doc">
<a name="lab51"></a><h2 class="section">The <span class="inlinecode"><span class="id" type="var">G</span></span> Monad</h2>

<div class="paragraph"> </div>

 In QuickChick, a generator for elements of some type <span class="inlinecode"><span class="id" type="var">A</span></span> belongs
    to the type <span class="inlinecode"><span class="id" type="var">G</span></span> <span class="inlinecode"><span class="id" type="var">A</span></span>.  Intuitively, this type describes functions
    that take a random seed to an element of <span class="inlinecode"><span class="id" type="var">A</span></span>.  We will see below
    that <span class="inlinecode"><span class="id" type="var">G</span></span> is actually a bit more than this, but this intuition will
    do for now. 
<div class="paragraph"> </div>

 QuickChick provides a number of primitives for building
    generators.  First, <span class="inlinecode"><span class="id" type="var">returnGen</span></span> takes a constant value and yields
    a generator that always returns this value. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Check</span> <span class="id" type="var">returnGen</span>.<br/>
</div>

<div class="doc">

<div class="paragraph"> </div>

<pre>     ===&gt; returnGen : ?A <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> G ?A 
</pre>

<div class="paragraph"> </div>

 We can see how it behaves by using the <span class="inlinecode"><span class="id" type="var">Sample</span></span> command, which
    supplies its generator argument with several different random
    seeds: 
</div>
<div class="code code-tight">

<span class="comment">(*&nbsp;Sample&nbsp;(returnGen&nbsp;42).&nbsp;*)</span><br/>
</div>

<div class="doc">
<pre>     ===&gt; [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42] 
</pre>

<div class="paragraph"> </div>

 Next, given a random generator for <span class="inlinecode"><span class="id" type="var">A</span></span> and a _function_ <span class="inlinecode"><span class="id" type="var">f</span></span> taking
    an <span class="inlinecode"><span class="id" type="var">A</span></span> and yielding a random generator for <span class="inlinecode"><span class="id" type="var">B</span></span>, we can plumb the
    two together into a generator for <span class="inlinecode"><span class="id" type="var">B</span></span> that works by internally
    generating a random <span class="inlinecode"><span class="id" type="var">A</span></span> and applying <span class="inlinecode"><span class="id" type="var">f</span></span> to it. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Check</span> <span class="id" type="var">bindGen</span>.<br/>
</div>

<div class="doc">
<pre>     ===&gt; bindGen : G ?A <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> (?A <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> G ?B) <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> G ?B 
</pre>

<div class="paragraph"> </div>

 Naturally, the implementation of <span class="inlinecode"><span class="id" type="var">bindGen</span></span> must take care
    to pass different random seeds to the two sub-generators! 
<div class="paragraph"> </div>

 With these two primitives in hand, we can make <span class="inlinecode"><span class="id" type="var">G</span></span> an instance of
    the <span class="inlinecode"><span class="id" type="var">Monad</span></span> typeclass. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Section</span> <span class="id" type="var">GMonadDef</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Instance</span> <span class="id" type="var">GMonad</span> : `{<span class="id" type="var">Monad</span> <span class="id" type="var">G</span>} | 3 :=<br/>
&nbsp;&nbsp;{<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">ret</span> := @<span class="id" type="var">returnGen</span>;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">bind</span> := @<span class="id" type="var">bindGen</span><br/>
&nbsp;&nbsp;}.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">End</span> <span class="id" type="var">GMonadDef</span>.<br/>
</div>

<div class="doc">
<a name="lab52"></a><h2 class="section">Primitive generators</h2>

<div class="paragraph"> </div>

 QuickChick provides several primitive generators for "ordered
    types," accessed via the <span class="inlinecode"><span class="id" type="var">choose</span></span> combinator. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Check</span> @<span class="id" type="var">choose</span>.<br/>
</div>

<div class="doc">
<pre>     ===&gt; 
     @choose
     : forall A : Type, ChoosableFromInterval A <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> A * A <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> G A 
</pre>

<div class="paragraph"> </div>

 The <span class="inlinecode"><span class="id" type="var">ChoosableFromInterval</span></span> typeclass describes primitive types
    <span class="inlinecode"><span class="id" type="var">A</span></span>, like natural numbers and integers (<span class="inlinecode"><span class="id" type="var">Z</span></span>), for which it makes
    sense to randomly generate elements from a given interval. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Print</span> <span class="id" type="var">ChoosableFromInterval</span>.<br/>
</div>

<div class="doc">
<pre>     ===&gt;
     Record ChoosableFromInterval (A : Type) : Type := 
       Build_ChoosableFromInterval
       { super : Ord A;
         randomR : A * A <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> RandomSeed <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> A * RandomSeed;
         ...
       }. 
</pre>

</div>
<div class="code code-tight">

<span class="comment">(*&nbsp;Sample&nbsp;(choose&nbsp;(0,10)).&nbsp;*)</span><br/>
</div>

<div class="doc">
<pre>     ===&gt; [ 1, 2, 1, 9, 8, 1, 3, 6, 2, 1, 8, 0, 1, 1, 3, 5, 4, 10, 4, 6 ] 
</pre>

<div class="paragraph"> </div>

<a name="lab53"></a><h4 class="section">练习：1 星, standard, optional (cfi)</h4>
 Print out the full definition of <span class="inlinecode"><span class="id" type="var">ChoosableFromInterval</span></span>.  Can you
    understand what it means?  <span class="proofbox">&#9744;</span> 
</div>

<div class="doc">
<a name="lab54"></a><h2 class="section">Lists</h2>

<div class="paragraph"> </div>

 Since they are a very commonly used compound datatype, lists have
    special combinators in QuickChick: <span class="inlinecode"><span class="id" type="var">listOf</span></span> and <span class="inlinecode"><span class="id" type="var">vectorOf</span></span>. 
<div class="paragraph"> </div>

 The <span class="inlinecode"><span class="id" type="var">listOf</span></span> combinator takes as input a generator for elements of
    type <span class="inlinecode"><span class="id" type="var">A</span></span> and returns a generator for lists of <span class="inlinecode"><span class="id" type="var">A</span></span>s. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Check</span> <span class="id" type="var">listOf</span>.<br/>
</div>

<div class="doc">
<pre>     ===&gt; listOf : G ?A <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> G (list ?A) 
</pre>

</div>
<div class="code code-tight">

<span class="comment">(*&nbsp;Sample&nbsp;(listOf&nbsp;(choose&nbsp;(0,4))).&nbsp;*)</span><br/>
</div>

<div class="doc">
<pre>     ===&gt; 
      [ [ 0, 3, 2, 0 ], 
        [ 1, 3, 4, 1, 0, 3, 0, 2, 2, 3, 2, 2, 2, 0, 4, 2, 3, 0, 1 ], 
        [ 3, 4, 3, 1, 2, 4, 4, 1, 0, 3, 4, 3, 2, 2, 4, 4, 1 ], 
        [ 0 ], 
        [ 4, 2, 3 ], 
        [ 3, 3, 4, 0, 1, 4, 3, 2, 4, 1 ], 
        [ 0, 4 ], 
        [  ], 
        [ 1, 0, 1, 3, 1 ], 
        [ 0, 0 ], 
        [ 1, 4 ], 
        [ 4, 3, 2, 0, 2, 2, 4, 0 ], 
        [ 1, 1, 0, 0, 1, 4 ], 
        [ 2, 0, 2, 1, 3, 3 ], 
        [ 4, 3, 3, 0, 1 ], 
        [ 3, 3, 3 ], 
        [ 3, 2, 4 ], 
        [ 1, 2 ], 
        [  ], 
        [  ] ] 
</pre>

<div class="paragraph"> </div>

 The second combinator, <span class="inlinecode"><span class="id" type="var">vectorOf</span></span>, receives an additional numeric
    argument <span class="inlinecode"><span class="id" type="var">n</span></span>, the length of the list to be generated. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Check</span> <span class="id" type="var">vectorOf</span>.<br/>
</div>

<div class="doc">
<pre>     ===&gt; vectorOf : nat <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> G ?A <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> G (list ?A) 
</pre>

</div>
<div class="code code-tight">

<span class="comment">(*&nbsp;Sample&nbsp;(vectorOf&nbsp;3&nbsp;(choose&nbsp;(0,4))).&nbsp;*)</span><br/>
</div>

<div class="doc">
<pre>     ===&gt; 
      [ [0, 1, 4], 
        [1, 1, 0], 
        [3, 3, 3], 
        [0, 2, 1], 
        [1, 3, 2], 
        [3, 3, 0], 
        [3, 0, 4], 
        [2, 3, 3], 
        [3, 2, 4], 
        [1, 2, 3], 
        [2, 0, 4]  ] 
</pre>

<div class="paragraph"> </div>

 This raises a question.  It's clear how <span class="inlinecode"><span class="id" type="var">vectorOf</span></span> decides how big
    to make its lists (we tell it!), but how does <span class="inlinecode"><span class="id" type="var">listOf</span></span> do it?  The
    answer is hidden inside <span class="inlinecode"><span class="id" type="var">G</span></span>.

<div class="paragraph"> </div>

    In addition to handling random-seed plumbing, the <span class="inlinecode"><span class="id" type="var">G</span></span> monad also
    maintains a "current maximum size" (in the style of a "reader
    monad", if you like that terminology): a natural number that
    can be used as an upper bound on the depth of generated objects. 
<div class="paragraph"> </div>

 Internally, <span class="inlinecode"><span class="id" type="var">G</span></span> <span class="inlinecode"><span class="id" type="var">A</span></span> is just a synonym for <span class="inlinecode"><span class="id" type="var">nat</span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" type="var">RandomSeed</span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" type="var">A</span></span>. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Module</span> <span class="id" type="var">DefineG</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Inductive</span> <span class="id" type="var">G</span> (<span class="id" type="var">A</span>:<span class="id" type="keyword">Type</span>) : <span class="id" type="keyword">Type</span> :=<br/>
| <span class="id" type="var">MkG</span> : (<span class="id" type="var">nat</span> → <span class="id" type="var">RandomSeed</span> → <span class="id" type="var">A</span>) → <span class="id" type="var">G</span> <span class="id" type="var">A</span>.<br/>
<span class="id" type="var">Arguments</span> <span class="id" type="var">MkG</span> {<span class="id" type="var">A</span>}.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">End</span> <span class="id" type="var">DefineG</span>.<br/>
</div>

<div class="doc">
When it is searching for counterexamples, QuickChick progressively
    tries larger and larger values for the size bound <span class="inlinecode"><span class="id" type="var">n</span></span>, to
    gradually explore deeper into the search space.

<div class="paragraph"> </div>

    Each generator can choose to interpret the size bound however it
    wants, and there is no _enforced_ guarantee that generators pay
    any attention to it at all; however, it is good practice to
    respect this bound when programming generators. 
</div>

<div class="doc">
<a name="lab55"></a><h2 class="section">Custom Generators</h2>

<div class="paragraph"> </div>

 Naturally, we also need generators for user-defined datatypes.
    Here's a simple one to play with: 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Inductive</span> <span class="id" type="var">color</span> := <span class="id" type="var">Red</span> | <span class="id" type="var">Green</span> | <span class="id" type="var">Blue</span> | <span class="id" type="var">Yellow</span>.<br/>
</div>

<div class="doc">
In order for commands like <span class="inlinecode"><span class="id" type="var">Sample</span></span> to display colors, we should
    make <span class="inlinecode"><span class="id" type="var">color</span></span> an instance of the <span class="inlinecode"><span class="id" type="keyword">Show</span></span> typeclass: 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Instance</span> <span class="id" type="var">show_color</span> : <span class="id" type="keyword">Show</span> <span class="id" type="var">color</span> :=<br/>
&nbsp;&nbsp;{| <span class="id" type="var">show</span> <span class="id" type="var">c</span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">match</span> <span class="id" type="var">c</span> <span class="id" type="keyword">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" type="var">Red</span>    ⇒ "Red"<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" type="var">Green</span>  ⇒ "Green"<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" type="var">Blue</span>   ⇒ "Blue"<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" type="var">Yellow</span> ⇒ "Yellow"<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">end</span><br/>
&nbsp;&nbsp;|}.<br/>
</div>

<div class="doc">
To generate a random color, we just need to pick one of the
    constructors <span class="inlinecode"><span class="id" type="var">Red</span></span>, <span class="inlinecode"><span class="id" type="var">Green</span></span>, <span class="inlinecode"><span class="id" type="var">Blue</span></span>, or <span class="inlinecode"><span class="id" type="var">Yellow</span></span>. This is done
    using <span class="inlinecode"><span class="id" type="var">elems_</span></span>. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Check</span> <span class="id" type="var">elems_</span>.<br/>
</div>

<div class="doc">
<pre>     ===&gt; elems_ : ?A <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> list ?A <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> G ?A 
</pre>

</div>
<div class="code code-tight">

<span class="id" type="keyword">Definition</span> <span class="id" type="var">genColor'</span> : <span class="id" type="var">G</span> <span class="id" type="var">color</span> :=<br/>
&nbsp;&nbsp;<span class="id" type="var">elems_</span> <span class="id" type="var">Red</span> [ <span class="id" type="var">Red</span> ; <span class="id" type="var">Green</span> ; <span class="id" type="var">Blue</span> ; <span class="id" type="var">Yellow</span> ].<br/><hr class='doublespaceincode'/>
<span class="comment">(*&nbsp;Sample&nbsp;genColor'.&nbsp;*)</span><br/>
</div>

<div class="doc">
<pre>     ===&gt; 
   [Red, Green, Blue, Blue, Red, Yellow, Blue, Red, Blue, Blue, Red] 
</pre>

<div class="paragraph"> </div>

 The first argument to <span class="inlinecode"><span class="id" type="var">elems_</span></span> serves as a default result.  If
    its list argument is not empty, <span class="inlinecode"><span class="id" type="var">elems_</span></span> returns a generator
    that always picks an element of that list; otherwise the generator
    always returns the default object.  This makes Coq's totality
    checker happy, but makes <span class="inlinecode"><span class="id" type="var">elem_</span></span> a little awkward to use, since
    typically its second argument will be a non-empty constant list. 
<div class="paragraph"> </div>

 To make the common case smoother, QuickChick provides convenient
    notations that automatically extract the default element. 
<div class="paragraph"> </div>


<div class="paragraph"> </div>

<pre>
     " 'elems' [ x ] " 
         := elems_ x (cons x nil)
     " 'elems' [ x ; y ] " 
         := elems_ x (cons x (cons y nil))
     " 'elems' [ x ; y ; .. ; z ] " 
         := elems_ x (cons x (cons y (.. (cons z nil))))
     " 'elems' ( x ;; l ) " 
         := elems_ x (cons x l)
</pre>

<div class="paragraph"> </div>

 Armed with <span class="inlinecode"><span class="id" type="var">elems</span></span>, we can write a <span class="inlinecode"><span class="id" type="var">color</span></span> generator the way we'd
    hope. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Definition</span> <span class="id" type="var">genColor</span> : <span class="id" type="var">G</span> <span class="id" type="var">color</span> :=<br/>
&nbsp;&nbsp;<span class="id" type="var">elems</span> [ <span class="id" type="var">Red</span> ; <span class="id" type="var">Green</span> ; <span class="id" type="var">Blue</span> ; <span class="id" type="var">Yellow</span> ].<br/><hr class='doublespaceincode'/>
<span class="comment">(*&nbsp;Sample&nbsp;genColor.&nbsp;*)</span><br/>
</div>

<div class="doc">
<pre>     ===&gt; [Red, Green, Blue, Blue, Red, Yellow, Blue, Red, Blue, Blue, Red] 
</pre>

<div class="paragraph"> </div>

 For more complicated ADTs, QuickChick provides more combinators.

<div class="paragraph"> </div>

    We showcase these using everyone's favorite datatype: trees! 
<div class="paragraph"> </div>

 Our trees are standard polymorphic binary trees; either <span class="inlinecode"><span class="id" type="var">Leaf</span></span>s or
    <span class="inlinecode"><span class="id" type="var">Node</span></span>s containing some payload of type <span class="inlinecode"><span class="id" type="var">A</span></span> and two subtrees. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Inductive</span> <span class="id" type="var">Tree</span> <span class="id" type="var">A</span> :=<br/>
| <span class="id" type="var">Leaf</span> : <span class="id" type="var">Tree</span> <span class="id" type="var">A</span><br/>
| <span class="id" type="var">Node</span> : <span class="id" type="var">A</span> → <span class="id" type="var">Tree</span> <span class="id" type="var">A</span> → <span class="id" type="var">Tree</span> <span class="id" type="var">A</span> → <span class="id" type="var">Tree</span> <span class="id" type="var">A</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="var">Arguments</span> <span class="id" type="var">Leaf</span> {<span class="id" type="var">A</span>}.<br/>
<span class="id" type="var">Arguments</span> <span class="id" type="var">Node</span> {<span class="id" type="var">A</span>} <span class="id" type="var">_</span> <span class="id" type="var">_</span> <span class="id" type="var">_</span>.<br/>
</div>

<div class="doc">
Before getting to generators for trees, we again give a
    straightforward <span class="inlinecode"><span class="id" type="keyword">Show</span></span> instance.  (The need for a local <span class="inlinecode"><span class="id" type="keyword">let</span></span> <span class="inlinecode"><span class="id" type="var">fix</span></span>
    declaration stems from the fact that Coq's typeclasses, unlike
    Haskell's, are not automatically recursive.  We could
    alternatively define <span class="inlinecode"><span class="id" type="var">aux</span></span> with a separate top-level
    <span class="inlinecode"><span class="id" type="keyword">Fixpoint</span></span>.) 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Instance</span> <span class="id" type="var">showTree</span> {<span class="id" type="var">A</span>} `{<span class="id" type="var">_</span> : <span class="id" type="keyword">Show</span> <span class="id" type="var">A</span>} : <span class="id" type="keyword">Show</span> (<span class="id" type="var">Tree</span> <span class="id" type="var">A</span>) :=<br/>
&nbsp;&nbsp;{| <span class="id" type="var">show</span> := <span class="id" type="keyword">let</span> <span class="id" type="var">fix</span> <span class="id" type="var">aux</span> <span class="id" type="var">t</span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">match</span> <span class="id" type="var">t</span> <span class="id" type="keyword">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" type="var">Leaf</span> ⇒ "Leaf"<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" type="var">Node</span> <span class="id" type="var">x</span> <span class="id" type="var">l</span> <span class="id" type="var">r</span> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;"Node (" ++ <span class="id" type="var">show</span> <span class="id" type="var">x</span> ++ ") (" <br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;++ <span class="id" type="var">aux</span> <span class="id" type="var">l</span> ++ ") (" <br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;++ <span class="id" type="var">aux</span> <span class="id" type="var">r</span> ++ ")"<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">end</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">in</span> <span class="id" type="var">aux</span><br/>
&nbsp;&nbsp;|}.<br/>
</div>

<div class="doc">
This brings us to our first generator _combinator_, called <span class="inlinecode"><span class="id" type="var">oneOf_</span></span>. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Check</span> <span class="id" type="var">oneOf_</span>.<br/>
</div>

<div class="doc">
<pre>     ===&gt; oneOf_ : G ?A <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> list (G ?A) <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> G ?A 
</pre>

<div class="paragraph"> </div>

 This combinator takes a default generator and a list of
    generators, and it picks one of the generators from the list
    uniformly at random (unless the list is empty, in which case it
    picks from the default generator).  As with <span class="inlinecode"><span class="id" type="var">elems_</span></span>, QuickChick
    introduces a more convenient notation <span class="inlinecode"><span class="id" type="var">oneOf</span></span> to hide this default
    element. 
<div class="paragraph"> </div>

 Next, Coq's termination checker will save us from shooting
    ourselves in the foot!

<div class="paragraph"> </div>

    The "obvious" first attempt at a generator is the following
    function <span class="inlinecode"><span class="id" type="var">genTree</span></span>, which generates either a <span class="inlinecode"><span class="id" type="var">Leaf</span></span> or else a
    <span class="inlinecode"><span class="id" type="var">Node</span></span> whose subtrees are generated recursively (and whose payload
    is produced by a generator <span class="inlinecode"><span class="id" type="var">g</span></span> for elements of type <span class="inlinecode"><span class="id" type="var">A</span></span>).
<div class="paragraph"> </div>


<div class="paragraph"> </div>

<pre>
     Fixpoint genTree {A} (g : G A) : G (Tree A) :=
        oneOf [ ret Leaf ;;
                liftM3 Node g (genTree g) (genTree g) ].
</pre>

<div class="paragraph"> </div>

 Of course, this fixpoint will not pass Coq's termination
    checker. Attempting to justify this fixpoint informally, one might
    first say that at some point the random generation will pick a
    <span class="inlinecode"><span class="id" type="var">Leaf</span></span> so it will eventually terminate.  But the termination
    checker cannot understand this kind of probabilistic reasoning.
    Moreover, even informally, the reasoning is wrong: Every time we
    choose to generate a <span class="inlinecode"><span class="id" type="var">Node</span></span>, we create two separate branches that
    must both be terminated with leaves.  It is not hard to show that
    the _expected_ size of the generated trees is actually
    infinite! 
<div class="paragraph"> </div>

 The solution is to use the standard "fuel" idiom that all Coq
    users know.  We add a natural number <span class="inlinecode"><span class="id" type="var">sz</span></span> as a parameter.  We
    decrease this size in each recursive call, and when it reaches
    <span class="inlinecode"><span class="id" type="var">O</span></span>, we always generate <span class="inlinecode"><span class="id" type="var">Leaf</span></span>.  Thus, the initial <span class="inlinecode"><span class="id" type="var">sz</span></span> parameter
    serves as a bound on the depth of the tree. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Fixpoint</span> <span class="id" type="var">genTreeSized</span> {<span class="id" type="var">A</span>} (<span class="id" type="var">sz</span> : <span class="id" type="var">nat</span>) (<span class="id" type="var">g</span> : <span class="id" type="var">G</span> <span class="id" type="var">A</span>) : <span class="id" type="var">G</span> (<span class="id" type="var">Tree</span> <span class="id" type="var">A</span>) :=<br/>
&nbsp;&nbsp;<span class="id" type="keyword">match</span> <span class="id" type="var">sz</span> <span class="id" type="keyword">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" type="var">O</span> ⇒ <span class="id" type="var">ret</span> <span class="id" type="var">Leaf</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" type="var">S</span> <span class="id" type="var">sz'</span> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">oneOf</span> [ <br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">ret</span> <span class="id" type="var">Leaf</span> ;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">liftM3</span> <span class="id" type="var">Node</span> <span class="id" type="var">g</span> (<span class="id" type="var">genTreeSized</span> <span class="id" type="var">sz'</span> <span class="id" type="var">g</span>) (<span class="id" type="var">genTreeSized</span> <span class="id" type="var">sz'</span> <span class="id" type="var">g</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;]<br/>
&nbsp;&nbsp;<span class="id" type="keyword">end</span>.<br/><hr class='doublespaceincode'/>
<span class="comment">(*&nbsp;Sample&nbsp;(genTreeSized&nbsp;3&nbsp;(choose(0,3))).&nbsp;*)</span><br/>
</div>

<div class="doc">
<pre>     ===&gt; 
       [ Leaf,
         Leaf,
         Node (3) (Node (0) (Leaf) (Leaf))
                  (Node (2) (Leaf) (Node (3) (Leaf) (Leaf))),
         Leaf,
         Leaf,
         Leaf,
         Node (1) (Leaf) (Node (1) (Leaf) (Node (0) (Leaf) (Leaf))),
         Leaf,
         Node (3) (Leaf) (Leaf),
         Node (1) (Leaf) (Leaf),
         Leaf,
         Leaf,
         Node (0) (Leaf) (Node (0) (Leaf) (Node (2) (Leaf) (Leaf))),
         Node (0) (Node (2) (Node (3) (Leaf) (Leaf)) (Leaf)) (Leaf),
         Node (0) (Leaf) (Leaf),
         Leaf,
         Leaf,
         Leaf,
         Leaf,
         Leaf ] 
</pre>

<div class="paragraph"> </div>

 While this generator succeeds in avoiding nontermination, we can
    see just by observing the result of <span class="inlinecode"><span class="id" type="var">Sample</span></span> that there is a
    problem: it produces way too many <span class="inlinecode"><span class="id" type="var">Leaf</span></span>s!  This is actually not
    surprising, since half the time we generate a <span class="inlinecode"><span class="id" type="var">Leaf</span></span> right at the
    outset.  
<div class="paragraph"> </div>

 We can obtain bigger trees more often if we skew the distribution
    towards <span class="inlinecode"><span class="id" type="var">Node</span></span>s using a more expressive QuickChick combinator,
    <span class="inlinecode"><span class="id" type="var">freq_</span></span>. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Check</span> <span class="id" type="var">freq_</span>.<br/>
</div>

<div class="doc">
<pre>     ===&gt; freq_ : G ?A <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> seq (nat * G ?A) <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> G ?A 
</pre>

<div class="paragraph"> </div>

 As with <span class="inlinecode"><span class="id" type="var">oneOf</span></span>, we usually use a convenient derived notation,
    called <span class="inlinecode"><span class="id" type="var">freq</span></span>, that takes a list of generators, each tagged with a
    natural number that serves as the weight of that generator.  For
    example, in the following generator, a <span class="inlinecode"><span class="id" type="var">Leaf</span></span> will be generated 1
    / (sz + 1) of the time and a <span class="inlinecode"><span class="id" type="var">Node</span></span> the remaining sz / (sz + 1) of
    the time. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Fixpoint</span> <span class="id" type="var">genTreeSized'</span> {<span class="id" type="var">A</span>} (<span class="id" type="var">sz</span> : <span class="id" type="var">nat</span>) (<span class="id" type="var">g</span> : <span class="id" type="var">G</span> <span class="id" type="var">A</span>) : <span class="id" type="var">G</span> (<span class="id" type="var">Tree</span> <span class="id" type="var">A</span>) :=<br/>
&nbsp;&nbsp;<span class="id" type="keyword">match</span> <span class="id" type="var">sz</span> <span class="id" type="keyword">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" type="var">O</span> ⇒ <span class="id" type="var">ret</span> <span class="id" type="var">Leaf</span> <br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" type="var">S</span> <span class="id" type="var">sz'</span> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">freq</span> [ (1,  <span class="id" type="var">ret</span> <span class="id" type="var">Leaf</span>) ;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">sz</span>, <span class="id" type="var">liftM3</span> <span class="id" type="var">Node</span> <span class="id" type="var">g</span> (<span class="id" type="var">genTreeSized'</span> <span class="id" type="var">sz'</span> <span class="id" type="var">g</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">genTreeSized'</span> <span class="id" type="var">sz'</span> <span class="id" type="var">g</span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;]<br/>
&nbsp;&nbsp;<span class="id" type="keyword">end</span>.<br/><hr class='doublespaceincode'/>
<span class="comment">(*&nbsp;Sample&nbsp;(genTreeSized'&nbsp;3&nbsp;(choose(0,3))).&nbsp;*)</span><br/>
</div>

<div class="doc">
<pre>     ===&gt; 
         [ Node (3) (Node (1) (Node (3) (Leaf) (Leaf)) (Leaf)) 
                    (Node (0) (Leaf) (Node (3) (Leaf) (Leaf))),
           Leaf,
           Node (2) (Node (1) (Leaf) (Leaf)) (Leaf),
           Node (0) (Leaf) (Node (0) (Node (2) (Leaf) (Leaf))
                                     (Node (0) (Leaf) (Leaf))),
           Node (1) (Node (2) (Leaf) (Node (0) (Leaf) (Leaf))) (Leaf),
           Node (0) (Node (0) (Leaf) (Node (3) (Leaf) (Leaf)))
                    (Node (2) (Leaf) (Leaf)),
           Node (1) (Node (3) (Node (2) (Leaf) (Leaf)) (Node (3) (Leaf) (Leaf)))
                    (Node (1) (Leaf) (Node (2) (Leaf) (Leaf))),
           Node (0) (Node (0) (Node (0) (Leaf) (Leaf)) (Node (1) (Leaf) (Leaf))) 
                    (Node (2) (Node (3) (Leaf) (Leaf)) (Node (0) (Leaf) (Leaf))),
           Node (2) (Node (2) (Leaf) (Leaf)) (Node (1) (Node (2) (Leaf) (Leaf))
                                                       (Node (2) (Leaf) (Leaf))),
           Node (2) (Node (3) (Node (2) (Leaf) (Leaf)) (Leaf)) 
                    (Node (0) (Node (2) (Leaf) (Leaf)) (Leaf)),
           Leaf,
           Node (2) (Node (3) (Node (3) (Leaf) (Leaf)) (Leaf)) (Leaf),
           Leaf,
           Node (1) (Leaf) (Leaf),
           Leaf,
           Node (1) (Node (2) (Leaf) (Node (3) (Leaf) (Leaf))) 
                    (Node (0) (Leaf) (Node (1) (Leaf) (Leaf))),
           Leaf,
           Node (3) (Node (0) (Node (0) (Leaf) (Leaf)) (Leaf)) 
                    (Node (0) (Leaf) (Node (2) (Leaf) (Leaf))),
           Node (2) (Node (2) (Node (0) (Leaf) (Leaf)) (Leaf)) 
                    (Node (1) (Leaf) (Node (2) (Leaf) (Leaf))),
           Leaf ] 
</pre>

<div class="paragraph"> </div>

 This looks better. 
<div class="paragraph"> </div>

<a name="lab56"></a><h4 class="section">练习：2 星, standard (genListSized)</h4>
 Write a sized generator for lists, following <span class="inlinecode"><span class="id" type="var">genTreeSized'</span></span>. 
</div>
<div class="code code-tight">

<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span><br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab57"></a><h4 class="section">练习：3 星, standard (genColorOption)</h4>
 Write a custom generator for values of type <span class="inlinecode"><span class="id" type="var">option</span></span> <span class="inlinecode"><span class="id" type="var">color</span></span>.  Make
    it generate <span class="inlinecode"><span class="id" type="var">None</span></span> about 1/10th of the time, and make it generate
    <span class="inlinecode"><span class="id" type="var">Some</span></span> <span class="inlinecode"><span class="id" type="var">Red</span></span> three times as often as the other colors. 
</div>
<div class="code code-tight">

<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span><br/>
</div>

<span class="proofbox">&#9744;</span> 

<div class="doc">
<a name="lab58"></a><h2 class="section">Checkers</h2>

<div class="paragraph"> </div>

 To showcase how such generators can be used to find
    counterexamples, suppose we define a function for "mirroring" a
    tree &mdash; swapping its left and right subtrees recursively. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Fixpoint</span> <span class="id" type="var">mirror</span> {<span class="id" type="var">A</span> : <span class="id" type="keyword">Type</span>} (<span class="id" type="var">t</span> : <span class="id" type="var">Tree</span> <span class="id" type="var">A</span>) : <span class="id" type="var">Tree</span> <span class="id" type="var">A</span> :=<br/>
&nbsp;&nbsp;<span class="id" type="keyword">match</span> <span class="id" type="var">t</span> <span class="id" type="keyword">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" type="var">Leaf</span> ⇒ <span class="id" type="var">Leaf</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" type="var">Node</span> <span class="id" type="var">x</span> <span class="id" type="var">l</span> <span class="id" type="var">r</span> ⇒ <span class="id" type="var">Node</span> <span class="id" type="var">x</span> (<span class="id" type="var">mirror</span> <span class="id" type="var">r</span>) (<span class="id" type="var">mirror</span> <span class="id" type="var">l</span>)<br/>
&nbsp;&nbsp;<span class="id" type="keyword">end</span>.<br/>
</div>

<div class="doc">
To formulate a property about <span class="inlinecode"><span class="id" type="var">mirror</span></span>, we need a structural
    equality test on trees.  We can obtain that with minimal effort
    using the <span class="inlinecode"><span class="id" type="var">Dec</span></span> typeclass and the <span class="inlinecode"><span class="id" type="var">dec_eq</span></span> tactic. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Instance</span> <span class="id" type="var">eq_dec_tree</span> (<span class="id" type="var">t<sub>1</sub></span> <span class="id" type="var">t<sub>2</sub></span> : <span class="id" type="var">Tree</span> <span class="id" type="var">nat</span>) : <span class="id" type="var">Dec</span> (<span class="id" type="var">t<sub>1</sub></span> = <span class="id" type="var">t<sub>2</sub></span>) := {}.<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="var">dec_eq</span>. <span class="id" type="keyword">Defined</span>.<br/>
</div>

<div class="doc">
We expect that mirroring a tree twice should yield the original
    tree.  
</div>
<div class="code code-tight">

<span class="id" type="keyword">Definition</span> <span class="id" type="var">mirrorP</span> (<span class="id" type="var">t</span> : <span class="id" type="var">Tree</span> <span class="id" type="var">nat</span>) := (<span class="id" type="var">mirror</span> (<span class="id" type="var">mirror</span> <span class="id" type="var">t</span>)) = <span class="id" type="var">t</span>?.<br/>
</div>

<div class="doc">
Now we want to use our generator to create a lot of random trees
    and, for each one, check whether <span class="inlinecode"><span class="id" type="var">mirrorP</span></span> returns <span class="inlinecode"><span class="id" type="var">true</span></span> or
    <span class="inlinecode"><span class="id" type="var">false</span></span>.

<div class="paragraph"> </div>

    Another way to say this is that we want to use <span class="inlinecode"><span class="id" type="var">mirrorP</span></span> to build
    a _generator for test results_.

<div class="paragraph"> </div>

    Let's see how this works. 
<div class="paragraph"> </div>

 (Let's open a playground module so we can show simplified
    versions of the actual QuickChick definitions.) 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Module</span> <span class="id" type="var">CheckerPlayground1</span>.<br/>
</div>

<div class="doc">
First, we need a type of test results &mdash; let's call it <span class="inlinecode"><span class="id" type="var">Result</span></span>.
    For the moment, think of <span class="inlinecode"><span class="id" type="var">Result</span></span> as just an enumerated type with
    constructors <span class="inlinecode"><span class="id" type="var">Success</span></span> and <span class="inlinecode"><span class="id" type="var">Failure</span></span>.  
</div>
<div class="code code-tight">

<span class="id" type="keyword">Inductive</span> <span class="id" type="var">Result</span> := <span class="id" type="var">Success</span> | <span class="id" type="var">Failure</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Instance</span> <span class="id" type="var">showResult</span> : <span class="id" type="keyword">Show</span> <span class="id" type="var">Result</span> :=<br/>
&nbsp;&nbsp;{<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">show</span> <span class="id" type="var">r</span> := <span class="id" type="keyword">match</span> <span class="id" type="var">r</span> <span class="id" type="keyword">with</span> <span class="id" type="var">Success</span> ⇒ "Success" | <span class="id" type="var">Failure</span> ⇒ "Failure" <span class="id" type="keyword">end</span><br/>
&nbsp;&nbsp;}.<br/>
</div>

<div class="doc">
Then we can define the type <span class="inlinecode"><span class="id" type="var">Checker</span></span> to be <span class="inlinecode"><span class="id" type="var">G</span></span> <span class="inlinecode"><span class="id" type="var">Result</span></span>. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Definition</span> <span class="id" type="var">Checker</span> := <span class="id" type="var">G</span> <span class="id" type="var">Result</span>.<br/>
</div>

<div class="doc">
That is, a <span class="inlinecode"><span class="id" type="var">Checker</span></span> embodies some way of performing a randomized
    test of the truth of some proposition, which, when applied to a
    random seed, will yield either <span class="inlinecode"><span class="id" type="var">Success</span></span> (meaning that the
    proposition survived this test) or <span class="inlinecode"><span class="id" type="var">Failure</span></span> (meaning that this
    test demonstrates that the proposition was false).

<div class="paragraph"> </div>

    Sampling a <span class="inlinecode"><span class="id" type="var">Checker</span></span> many times with different seeds will cause
    many different tests to be performed. 
<div class="paragraph"> </div>

 To check <span class="inlinecode"><span class="id" type="var">mirrorP</span></span>, we'll need a way to build a <span class="inlinecode"><span class="id" type="var">Checker</span></span> out of a
    function from trees to booleans.

<div class="paragraph"> </div>

    Actually, we will be wanting to build <span class="inlinecode"><span class="id" type="var">Checker</span></span>s based on many
    different types.  So let's begin by defining a typeclass
    <span class="inlinecode"><span class="id" type="var">Checkable</span></span>, where an instance for <span class="inlinecode"><span class="id" type="var">Checkable</span></span> <span class="inlinecode"><span class="id" type="var">A</span></span> will provide a
    way of converting an <span class="inlinecode"><span class="id" type="var">A</span></span> into a <span class="inlinecode"><span class="id" type="var">Checker</span></span>. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Class</span> <span class="id" type="var">Checkable</span> <span class="id" type="var">A</span> :=<br/>
&nbsp;&nbsp;{<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">checker</span> : <span class="id" type="var">A</span> → <span class="id" type="var">Checker</span><br/>
&nbsp;&nbsp;}.<br/>
</div>

<div class="doc">
It is easy to give a <span class="inlinecode"><span class="id" type="var">bool</span></span> instance for <span class="inlinecode"><span class="id" type="var">Checkable</span></span>. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Instance</span> <span class="id" type="var">checkableBool</span> : <span class="id" type="var">Checkable</span> <span class="id" type="var">bool</span> :=<br/>
&nbsp;&nbsp;{<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">checker</span> <span class="id" type="var">b</span> := <span class="id" type="keyword">if</span> <span class="id" type="var">b</span> <span class="id" type="keyword">then</span> <span class="id" type="var">ret</span> <span class="id" type="var">Success</span> <span class="id" type="keyword">else</span> <span class="id" type="var">ret</span> <span class="id" type="var">Failure</span><br/>
&nbsp;&nbsp;}.<br/>
</div>

<div class="doc">
That is, the boolean value <span class="inlinecode"><span class="id" type="var">true</span></span> passes every test we might
    subject it to (i.e., the result of <span class="inlinecode"><span class="id" type="var">checker</span></span> is a <span class="inlinecode"><span class="id" type="var">G</span></span> that returns
    <span class="inlinecode"><span class="id" type="var">true</span></span> for every seed), while <span class="inlinecode"><span class="id" type="var">false</span></span> fails all tests. 
<div class="paragraph"> </div>

 Let's see what happens if we sample checkers for our favorite
    booleans, <span class="inlinecode"><span class="id" type="var">true</span></span> and <span class="inlinecode"><span class="id" type="var">false</span></span>.  
<div class="paragraph"> </div>

 (We need to exit the playground so that we can do <span class="inlinecode"><span class="id" type="var">Sample</span></span>:
    because <span class="inlinecode"><span class="id" type="var">Sample</span></span> is implemented internally via extraction to
    OCaml, which usually does not work from inside a <span class="inlinecode"><span class="id" type="keyword">Module</span></span>.) 
</div>
<div class="code code-tight">

<span class="id" type="keyword">End</span> <span class="id" type="var">CheckerPlayground1</span>.<br/><hr class='doublespaceincode'/>
<span class="comment">(*&nbsp;Sample&nbsp;(CheckerPlayground1.checker&nbsp;true).&nbsp;*)</span><br/>
</div>

<div class="doc">
<pre>     ===&gt;
      [Success, Success, Success, Success, Success, Success, Success, 
       Success, Success, Success, Success] 
</pre>

</div>
<div class="code code-tight">

<span class="comment">(*&nbsp;Sample&nbsp;(CheckerPlayground1.checker&nbsp;false).&nbsp;*)</span><br/>
</div>

<div class="doc">
<pre>     ===&gt;
      [Failure, Failure, Failure, Failure, Failure, Failure, Failure, 
       Failure, Failure, Failure, Failure] 
</pre>

<div class="paragraph"> </div>

 What we've done so far may look a a bit strange, since these
    checkers always generate the same results.  We'll make things more
    interesting in a bit, but first let's pause to define one more
    basic instance of <span class="inlinecode"><span class="id" type="var">Checkable</span></span>. 
<div class="paragraph"> </div>

 A decidable <span class="inlinecode"><span class="id" type="keyword">Prop</span></span> is not too different from a boolean, so we
    should be able to build a checker from that too. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Module</span> <span class="id" type="var">CheckerPlayground2</span>.<br/>
<span class="id" type="keyword">Export</span> <span class="id" type="var">CheckerPlayground1</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Instance</span> <span class="id" type="var">checkableDec</span> `{<span class="id" type="var">P</span> : <span class="id" type="keyword">Prop</span>} `{<span class="id" type="var">Dec</span> <span class="id" type="var">P</span>} : <span class="id" type="var">Checkable</span> <span class="id" type="var">P</span> :=<br/>
&nbsp;&nbsp;{<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">checker</span> <span class="id" type="var">p</span> := <span class="id" type="keyword">if</span> <span class="id" type="var">P</span>? <span class="id" type="keyword">then</span> <span class="id" type="var">ret</span> <span class="id" type="var">Success</span> <span class="id" type="keyword">else</span> <span class="id" type="var">ret</span> <span class="id" type="var">Failure</span><br/>
&nbsp;&nbsp;}.<br/>
</div>

<div class="doc">
(The definition looks a bit strange since it doesn't use its
    argument <span class="inlinecode"><span class="id" type="var">p</span></span>.  The intuition is that all the information in <span class="inlinecode"><span class="id" type="var">p</span></span> is
    already encoded in <span class="inlinecode"><span class="id" type="var">P</span></span>!) 
<div class="paragraph"> </div>

 Now suppose we pose a couple of (decidable) conjectures: 
</div>
<div class="code code-tight">

<span class="id" type="var">Conjecture</span> <span class="id" type="var">c<sub>1</sub></span> : 0 = 42.<br/>
<span class="id" type="var">Conjecture</span> <span class="id" type="var">c<sub>2</sub></span> : 41 + 1 = 42.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">End</span> <span class="id" type="var">CheckerPlayground2</span>.<br/>
</div>

<div class="doc">
The somewhat astononishing thing about the <span class="inlinecode"><span class="id" type="var">Checkable</span></span> instance
    for decidable <span class="inlinecode"><span class="id" type="keyword">Prop</span></span>s is that, even though these are
    _conjectures_ (we haven't proved them, so the "evidence" that Coq
    has for them internally is just an uninstantiated "evar"), we can
    still build checkers from them and sample from these
    checkers! (Why?  Technically, it is because the <span class="inlinecode"><span class="id" type="var">Checkable</span></span>
    instance for decidable properties does not look at its
    argument.) 
</div>
<div class="code code-tight">

<span class="comment">(*&nbsp;&nbsp;Sample&nbsp;(CheckerPlayground1.checker&nbsp;CheckerPlayground2.c1).&nbsp;*)</span><br/>
</div>

<div class="doc">
<pre>     ===&gt;
      [Failure, Failure, Failure, Failure, Failure, Failure, Failure, 
       Failure, Failure, Failure, Failure] 
</pre>

</div>
<div class="code code-tight">

<span class="comment">(*&nbsp;Sample&nbsp;(CheckerPlayground1.checker&nbsp;CheckerPlayground2.c2).&nbsp;*)</span><br/>
</div>

<div class="doc">
<pre>     ===&gt;
      [Success, Success, Success, Success, Success, Success, Success, 
       Success, Success, Success, Success] 
</pre>

<div class="paragraph"> </div>

 Again, the intuition is that, although we didn't present
    proofs (and could not have, in the first case!), Coq already
    "knows" either a proof or a disproof of each of these conjectures
    because they are decidable. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Module</span> <span class="id" type="var">CheckerPlayground3</span>.<br/>
<span class="id" type="keyword">Import</span> <span class="id" type="var">CheckerPlayground2</span>.<br/>
</div>

<div class="doc">
Now let's go back to <span class="inlinecode"><span class="id" type="var">mirrorP</span></span>.

<div class="paragraph"> </div>

    We have seen that the result of <span class="inlinecode"><span class="id" type="var">mirrorP</span></span> is <span class="inlinecode"><span class="id" type="var">Checkable</span></span>.  What we
    need is a way to take a function returning a checkable thing and
    make the function itself checkable.

<div class="paragraph"> </div>

    We can easily do this, as long as the argument type of the
    function is something we know how to generate! 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Definition</span> <span class="id" type="var">forAll</span> {<span class="id" type="var">A</span> <span class="id" type="var">B</span> : <span class="id" type="keyword">Type</span>} `{<span class="id" type="var">Checkable</span> <span class="id" type="var">B</span>}<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">g</span> : <span class="id" type="var">G</span> <span class="id" type="var">A</span>) (<span class="id" type="var">f</span> : <span class="id" type="var">A</span> → <span class="id" type="var">B</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;: <span class="id" type="var">Checker</span> :=<br/>
&nbsp;&nbsp;<span class="id" type="var">a</span> &lt;- <span class="id" type="var">g</span> ;;<br/>
&nbsp;&nbsp;<span class="id" type="var">checker</span> (<span class="id" type="var">f</span> <span class="id" type="var">a</span>).<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">End</span> <span class="id" type="var">CheckerPlayground3</span>.<br/>
</div>

<div class="doc">
Let's try this out.  We can define a boolean test that returns <span class="inlinecode"><span class="id" type="var">true</span></span>
    for <span class="inlinecode"><span class="id" type="var">Red</span></span> and <span class="inlinecode"><span class="id" type="var">false</span></span> for other colors. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Definition</span> <span class="id" type="var">isRed</span> <span class="id" type="var">c</span> := <br/>
&nbsp;&nbsp;<span class="id" type="keyword">match</span> <span class="id" type="var">c</span> <span class="id" type="keyword">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Red</span> ⇒ <span class="id" type="var">true</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">_</span> ⇒ <span class="id" type="var">false</span><br/>
&nbsp;&nbsp;<span class="id" type="keyword">end</span>.<br/>
</div>

<div class="doc">
Since we can generate elements of <span class="inlinecode"><span class="id" type="var">color</span></span> and we have a
    <span class="inlinecode"><span class="id" type="var">Checkable</span></span> instance for <span class="inlinecode"><span class="id" type="var">bool</span></span>, we can apply <span class="inlinecode"><span class="id" type="var">forAll</span></span> to <span class="inlinecode"><span class="id" type="var">isRed</span></span>
    and sample from the resulting <span class="inlinecode"><span class="id" type="var">Checker</span></span> to run some tests. 
</div>
<div class="code code-tight">

<span class="comment">(*&nbsp;Sample&nbsp;(CheckerPlayground3.forAll&nbsp;genColor&nbsp;isRed).&nbsp;*)</span><br/>
</div>

<div class="doc">
<pre>     ===&gt;
      [Success, Failure, Failure, Failure, Success, Failure, 
       Failure, Success, Failure, Failure, Success] 
</pre>

<div class="paragraph"> </div>

 Looks like not all colors are <span class="inlinecode"><span class="id" type="var">Red</span></span>.  

<div class="paragraph"> </div>

    Good to know. 
<div class="paragraph"> </div>

 Now, what about <span class="inlinecode"><span class="id" type="var">mirrorP</span></span>? 
</div>
<div class="code code-tight">

<span class="comment">(*<br/>
Sample&nbsp;(CheckerPlayground3.forAll<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(genTreeSized'&nbsp;3&nbsp;(choose(0,3)))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;mirrorP).<br/>
*)</span><br/>
</div>

<div class="doc">
<pre>     ===&gt;
      [Success, Success, Success, Success, Success, Success, Success, 
       Success, Success, Success, Success] 
</pre>

<div class="paragraph"> </div>

 Excellent: It looks like many tests are succeeding &mdash; maybe the
    property is true. 
<div class="paragraph"> </div>

 Let's instead try defining a bad property and see if we can detect
    that it's bad... 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Definition</span> <span class="id" type="var">faultyMirrorP</span> (<span class="id" type="var">t</span> : <span class="id" type="var">Tree</span> <span class="id" type="var">nat</span>) := (<span class="id" type="var">mirror</span> <span class="id" type="var">t</span>) = <span class="id" type="var">t</span> ?.<br/><hr class='doublespaceincode'/>
<span class="comment">(*<br/>
Sample&nbsp;(CheckerPlayground3.forAll<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(genTreeSized'&nbsp;3&nbsp;(choose(0,3)))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;faultyMirrorP).<br/>
*)</span><br/>
</div>

<div class="doc">
<pre>     ===&gt;
      [Failure, Success, Failure, Success, Success, Success, Failure, 
       Success, Failure, Failure, Success] 
</pre>

<div class="paragraph"> </div>

 Great &mdash; looks like a good number of tests are failing now, as
    expected. 
<div class="paragraph"> </div>

 There's only one little issue: What _are_ the tests that are
    failing?  We can tell by looking at the samples that the property
    is bad, but we can't see the counterexamples!

<div class="paragraph"> </div>

    We can fix this by going back to the beginning and enriching the
    <span class="inlinecode"><span class="id" type="var">Result</span></span> type to keep track of failing counterexamples. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Module</span> <span class="id" type="var">CheckerPlayground4</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Inductive</span> <span class="id" type="var">Result</span> :=<br/>
&nbsp;&nbsp;| <span class="id" type="var">Success</span> : <span class="id" type="var">Result</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">Failure</span> : <span style='font-size:120%;'>&forall;</span>{<span class="id" type="var">A</span>} `{<span class="id" type="keyword">Show</span> <span class="id" type="var">A</span>}, <span class="id" type="var">A</span> → <span class="id" type="var">Result</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Instance</span> <span class="id" type="var">showResult</span> : <span class="id" type="keyword">Show</span> <span class="id" type="var">Result</span> :=<br/>
&nbsp;&nbsp;{<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">show</span> <span class="id" type="var">r</span> := <span class="id" type="keyword">match</span> <span class="id" type="var">r</span> <span class="id" type="keyword">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Success</span> ⇒ "Success"<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" type="var">Failure</span> <span class="id" type="var">a</span> ⇒ "Failure: " ++ <span class="id" type="var">show</span> <span class="id" type="var">a</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">end</span><br/>
&nbsp;&nbsp;}.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">Checker</span> := <span class="id" type="var">G</span> <span class="id" type="var">Result</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Class</span> <span class="id" type="var">Checkable</span> <span class="id" type="var">A</span> :=<br/>
&nbsp;&nbsp;{<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">checker</span> : <span class="id" type="var">A</span> → <span class="id" type="var">Checker</span><br/>
&nbsp;&nbsp;}.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Instance</span> <span class="id" type="var">showUnit</span> : <span class="id" type="keyword">Show</span> <span class="id" type="var">unit</span> :=<br/>
&nbsp;&nbsp;{<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">show</span> <span class="id" type="var">u</span> := "tt"<br/>
&nbsp;&nbsp;}.<br/>
</div>

<div class="doc">
The failure cases in the <span class="inlinecode"><span class="id" type="var">bool</span></span> and <span class="inlinecode"><span class="id" type="var">Dec</span></span> checkers don't need to
    record anything except the <span class="inlinecode"><span class="id" type="var">Failure</span></span>, so we put <span class="inlinecode"><span class="id" type="var">tt</span></span> (the sole
    value of type <span class="inlinecode"><span class="id" type="var">unit</span></span>) as the "failure reason." 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Instance</span> <span class="id" type="var">checkableBool</span> : <span class="id" type="var">Checkable</span> <span class="id" type="var">bool</span> :=<br/>
&nbsp;&nbsp;{<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">checker</span> <span class="id" type="var">b</span> := <span class="id" type="keyword">if</span> <span class="id" type="var">b</span> <span class="id" type="keyword">then</span> <span class="id" type="var">ret</span> <span class="id" type="var">Success</span> <span class="id" type="keyword">else</span> <span class="id" type="var">ret</span> (<span class="id" type="var">Failure</span> <span class="id" type="var">tt</span>)<br/>
&nbsp;&nbsp;}.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Instance</span> <span class="id" type="var">checkableDec</span> `{<span class="id" type="var">P</span> : <span class="id" type="keyword">Prop</span>} `{<span class="id" type="var">Dec</span> <span class="id" type="var">P</span>} : <span class="id" type="var">Checkable</span> <span class="id" type="var">P</span> :=<br/>
&nbsp;&nbsp;{<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">checker</span> <span class="id" type="var">p</span> := <span class="id" type="keyword">if</span> <span class="id" type="var">P</span>? <span class="id" type="keyword">then</span> <span class="id" type="var">ret</span> <span class="id" type="var">Success</span> <span class="id" type="keyword">else</span> <span class="id" type="var">ret</span> (<span class="id" type="var">Failure</span> <span class="id" type="var">tt</span>)<br/>
&nbsp;&nbsp;}.<br/>
</div>

<div class="doc">
The interesting case is the <span class="inlinecode"><span class="id" type="var">forAll</span></span> combinator.  Here, we _do_
    have some useful information to record in the failure case &mdash;
    namely, the argument that caused the failure. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Definition</span> <span class="id" type="var">forAll</span> {<span class="id" type="var">A</span> <span class="id" type="var">B</span> : <span class="id" type="keyword">Type</span>} `{<span class="id" type="keyword">Show</span> <span class="id" type="var">A</span>} `{<span class="id" type="var">Checkable</span> <span class="id" type="var">B</span>}<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">g</span> : <span class="id" type="var">G</span> <span class="id" type="var">A</span>) (<span class="id" type="var">f</span> : <span class="id" type="var">A</span> → <span class="id" type="var">B</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;: <span class="id" type="var">Checker</span> :=<br/>
&nbsp;&nbsp;<span class="id" type="var">a</span> &lt;- <span class="id" type="var">g</span> ;;<br/>
&nbsp;&nbsp;<span class="id" type="var">r</span> &lt;- <span class="id" type="var">checker</span> (<span class="id" type="var">f</span> <span class="id" type="var">a</span>) ;;<br/>
&nbsp;&nbsp;<span class="id" type="keyword">match</span> <span class="id" type="var">r</span> <span class="id" type="keyword">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Success</span> ⇒ <span class="id" type="var">ret</span> <span class="id" type="var">Success</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">Failure</span> <span class="id" type="var">b</span> ⇒ <span class="id" type="var">ret</span> (<span class="id" type="var">Failure</span> (<span class="id" type="var">a</span>,<span class="id" type="var">b</span>))<br/>
&nbsp;&nbsp;<span class="id" type="keyword">end</span>.<br/>
</div>

<div class="doc">
Note that, rather than just returning <span class="inlinecode"><span class="id" type="var">Failure</span></span> <span class="inlinecode"><span class="id" type="var">a</span></span>, we package up
    <span class="inlinecode"><span class="id" type="var">a</span></span> together with <span class="inlinecode"><span class="id" type="var">b</span></span>, which explains the reason for the failure
    of <span class="inlinecode"><span class="id" type="var">f</span></span> <span class="inlinecode"><span class="id" type="var">a</span></span>.  This allows us to write several <span class="inlinecode"><span class="id" type="var">forAll</span></span>s in sequence
    and capture all of their results in a nested tuple. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">End</span> <span class="id" type="var">CheckerPlayground4</span>.<br/><hr class='doublespaceincode'/>
<span class="comment">(*<br/>
Sample&nbsp;(CheckerPlayground4.forAll<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(genTreeSized'&nbsp;3&nbsp;(choose(0,3)))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;faultyMirrorP).<br/>
*)</span><br/>
</div>

<div class="doc">
<pre>     ===&gt;
      [Failure: (Node (2) (Node (3) (Node (2) (Leaf) (Leaf)) (Leaf)) 
                          (Node (0) (Node (2) (Leaf) (Leaf)) (Leaf)), tt), 
      Success, 
      Failure: (Node (2) (Node (3) (Node (3) (Leaf) (Leaf)) (Leaf)) (Leaf), tt), 
      Success, Success, Success, 
      Failure: (Node (1) (Node (2) (Leaf) (Node (3) (Leaf) (Leaf))) 
                         (Node (0) (Leaf) (Node (1) (Leaf) (Leaf))), tt), 
      Success, 
      Failure: (Node (3) (Node (0) (Node (0) (Leaf) (Leaf)) (Leaf)) 
                         (Node (0) (Leaf) (Node (2) (Leaf) (Leaf))), tt), 
      Failure: (Node (2) (Node (2) (Node (0) (Leaf) (Leaf)) (Leaf)) 
                         (Node (1) (Leaf) (Node (2) (Leaf) (Leaf))), tt), 
      Success] 
</pre>

<div class="paragraph"> </div>

 The bug is found several times and actual counterexamples are
    reported: nice! 
<div class="paragraph"> </div>

 Sampling repeatedly from a generator is just what the <span class="inlinecode"><span class="id" type="var">QuickChick</span></span>
    command does, except that, instead of running a fixed number of
    tests and returning their results in a list, it runs tests only
    until the first counterexample is found. 
</div>
<div class="code code-tight">

<span class="comment">(*<br/>
QuickChick<br/>
&nbsp;&nbsp;(forAll<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(genTreeSized'&nbsp;3&nbsp;(choose(0,3)))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;faultyMirrorP).<br/>
*)</span><br/>
</div>

<div class="doc">
<pre>     ===&gt;
     QuickChecking (forAll (genTreeSized' 3 (choose (0, 3))) faultyMirrorP)

     Node (0) (Node (0) (Node (2) (Leaf) (Leaf)) 
                        (Node (1) (Leaf) (Leaf)))
              (Node (1) (Node (0) (Leaf) (Leaf)) (Leaf))

     *** Failed after 1 tests and 0 shrinks. (0 discards) 
</pre>

<div class="paragraph"> </div>

 However, these counterexamples themselves still leave something to
    be desired: they are all _much_ larger than is really needed to
    illustrate the bad behavior of <span class="inlinecode"><span class="id" type="var">faultyMirrorP</span></span>.

<div class="paragraph"> </div>

    This is where _shrinking_ comes in. 
</div>

<div class="doc">
<a name="lab59"></a><h1 class="section">Shrinking</h1>

<div class="paragraph"> </div>

 Shrinking (sometimes known as "delta debugging") is a process
    that, given a counterexample to some property, searches (greedily)
    for smaller counterexamples.

<div class="paragraph"> </div>

    Given a shrinking function <span class="inlinecode"><span class="id" type="var">s</span></span> of type <span class="inlinecode"><span class="id" type="var">A</span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" type="var">list</span></span> <span class="inlinecode"><span class="id" type="var">A</span></span> and a value
    <span class="inlinecode"><span class="id" type="var">x</span></span> of type <span class="inlinecode"><span class="id" type="var">A</span></span> that is known to falsify some property <span class="inlinecode"><span class="id" type="var">P</span></span>,
    QuickChick tries <span class="inlinecode"><span class="id" type="var">P</span></span> on all members of <span class="inlinecode"><span class="id" type="var">s</span></span> <span class="inlinecode"><span class="id" type="var">x</span></span> until it finds
    another counterexample.  It repeats this process, starting from
    the new counterexample, until it reaches a point where <span class="inlinecode"><span class="id" type="var">x</span></span> fails
    property <span class="inlinecode"><span class="id" type="var">P</span></span> but every element of <span class="inlinecode"><span class="id" type="var">s</span></span> <span class="inlinecode"><span class="id" type="var">x</span></span> succeeds.  This <span class="inlinecode"><span class="id" type="var">x</span></span> is a
    "locally minimal" counterexample. 
<div class="paragraph"> </div>

 Clearly, this greedy algorithm only work if all elements of
    <span class="inlinecode"><span class="id" type="var">s</span></span> <span class="inlinecode"><span class="id" type="var">x</span></span> are strictly "smaller" than <span class="inlinecode"><span class="id" type="var">x</span></span> for all <span class="inlinecode"><span class="id" type="var">x</span></span> &mdash; that is,
    there should be some total order on the type of <span class="inlinecode"><span class="id" type="var">x</span></span> such that <span class="inlinecode"><span class="id" type="var">s</span></span>
    is strictly decreasing in this order.  This is the basic
    correctness requirement for a shrinker.  It is guaranteed by all
    the shrinkers that QuickChick derives automatically, but ifyou
    roll your own shrinkers you need to be careful to maintain it. 
<div class="paragraph"> </div>

 Here is a shrinker for <span class="inlinecode"><span class="id" type="var">color</span></span>s. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Instance</span> <span class="id" type="var">shrinkColor</span> : <span class="id" type="var">Shrink</span> <span class="id" type="var">color</span> :=<br/>
&nbsp;&nbsp;{<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">shrink</span> <span class="id" type="var">c</span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">match</span> <span class="id" type="var">c</span> <span class="id" type="keyword">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" type="var">Red</span> ⇒ [ ]<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" type="var">Green</span> ⇒ [ <span class="id" type="var">Red</span> ]<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" type="var">Blue</span> ⇒ [ <span class="id" type="var">Red</span>; <span class="id" type="var">Green</span> ]<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" type="var">Yellow</span> ⇒ [ <span class="id" type="var">Red</span>; <span class="id" type="var">Green</span>; <span class="id" type="var">Blue</span> ]<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">end</span><br/>
&nbsp;&nbsp;}.<br/>
</div>

<div class="doc">
Most of the time, shrinking functions should try to return
    elements that are "just one step" smaller than the one they are
    given. For example, consider the default shrinking function for
    lists provided by QuickChick. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Print</span> <span class="id" type="var">shrinkList</span>.<br/>
</div>

<div class="doc">
<pre>     ===&gt; 
       shrinkList = 
         fun (A : Type) (H : Shrink A) =&gt; 
            {| shrink := shrinkListAux shrink |}
       : forall A : Type, Shrink A <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> Shrink (list A) 

</pre>

</div>
<div class="code code-tight">

<span class="id" type="keyword">Print</span> <span class="id" type="var">shrinkListAux</span>.<br/>
</div>

<div class="doc">
<pre>     ===&gt; 
       shrinkListAux = 
         fix shrinkListAux (A : Type) (shr : A <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> list A) (l : list A) :
           list (list A) :=
           match l with
           | [] =&gt; []
           | x :: xs =&gt;
               ((xs :: map (fun xs' : list A =&gt; x :: xs') 
                           (shrinkListAux A shr xs)) ++
                map (fun x' : A =&gt; x' :: xs) (shr x))
           end
       : forall A : Type, (A <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> list A) <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> list A <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> list (list A) 
</pre>

<div class="paragraph"> </div>

 An empty list cannot be shrunk, as there is no smaller list.  A
    cons cell can be shrunk in three ways: by returning the tail of
    the list, by shrinking the tail of the list and keeping the same
    head, or by shrinking the head and keeping the same tail. By
    induction, this process can generate all smaller lists.

<div class="paragraph"> </div>

    (Pro tip: One refinement to the advice that shrinkers should
    return "one step smaller" values is that, for potentially large
    data structures, it can sometimes greatly improve performance if a
    shrinker returns not only all the "slightly smaller" structures
    but also one or two "much smaller" structures.  E.g. for a number
    <span class="inlinecode"><span class="id" type="var">x</span></span> greater than <span class="inlinecode">2</span>, we might shrink to <span class="inlinecode">0;</span> <span class="inlinecode"><span class="id" type="var">x</span></span> <span class="inlinecode"><span class="id" type="var">div</span></span> <span class="inlinecode">2;</span> <span class="inlinecode"><span class="id" type="var">pred</span></span> <span class="inlinecode"><span class="id" type="var">x</span></span>.) 
<div class="paragraph"> </div>

 Writing a shrinking instance for trees is equally straightforward:
    we don't shrink <span class="inlinecode"><span class="id" type="var">Leaf</span></span>s, while for <span class="inlinecode"><span class="id" type="var">Node</span></span>s we can either return
    the left or right subtree, or shrink the payload, or shrink one of
    the subtrees. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Open</span> <span class="id" type="keyword">Scope</span> <span class="id" type="var">list</span>.<br/>
<span class="id" type="keyword">Fixpoint</span> <span class="id" type="var">shrinkTreeAux</span> {<span class="id" type="var">A</span>} <br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">s</span> : <span class="id" type="var">A</span> → <span class="id" type="var">list</span> <span class="id" type="var">A</span>) (<span class="id" type="var">t</span> : <span class="id" type="var">Tree</span> <span class="id" type="var">A</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;: <span class="id" type="var">list</span> (<span class="id" type="var">Tree</span> <span class="id" type="var">A</span>) :=<br/>
&nbsp;&nbsp;<span class="id" type="keyword">match</span> <span class="id" type="var">t</span> <span class="id" type="keyword">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" type="var">Leaf</span> ⇒ []<br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" type="var">Node</span> <span class="id" type="var">x</span> <span class="id" type="var">l</span> <span class="id" type="var">r</span> ⇒ [<span class="id" type="var">l</span>] ++ [<span class="id" type="var">r</span>] ++<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">map</span> (<span class="id" type="keyword">fun</span> <span class="id" type="var">x'</span> ⇒ <span class="id" type="var">Node</span> <span class="id" type="var">x'</span> <span class="id" type="var">l</span> <span class="id" type="var">r</span>) (<span class="id" type="var">s</span> <span class="id" type="var">x</span>) ++<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">map</span> (<span class="id" type="keyword">fun</span> <span class="id" type="var">l'</span> ⇒ <span class="id" type="var">Node</span> <span class="id" type="var">x</span> <span class="id" type="var">l'</span> <span class="id" type="var">r</span>) (<span class="id" type="var">shrinkTreeAux</span> <span class="id" type="var">s</span> <span class="id" type="var">l</span>) ++<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">map</span> (<span class="id" type="keyword">fun</span> <span class="id" type="var">r'</span> ⇒ <span class="id" type="var">Node</span> <span class="id" type="var">x</span> <span class="id" type="var">l</span> <span class="id" type="var">r'</span>) (<span class="id" type="var">shrinkTreeAux</span> <span class="id" type="var">s</span> <span class="id" type="var">r</span>)<br/>
&nbsp;&nbsp;<span class="id" type="keyword">end</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Instance</span> <span class="id" type="var">shrinkTree</span> {<span class="id" type="var">A</span>} `{<span class="id" type="var">Shrink</span> <span class="id" type="var">A</span>} : <span class="id" type="var">Shrink</span> (<span class="id" type="var">Tree</span> <span class="id" type="var">A</span>) := <br/>
&nbsp;&nbsp;{| <span class="id" type="var">shrink</span> <span class="id" type="var">x</span> := <span class="id" type="var">shrinkTreeAux</span> <span class="id" type="var">shrink</span> <span class="id" type="var">x</span> |}.<br/>
</div>

<div class="doc">
With <span class="inlinecode"><span class="id" type="var">shrinkTree</span></span> in hand, we can use the <span class="inlinecode"><span class="id" type="var">forAllShrink</span></span> property
    combinator, a variant of <span class="inlinecode"><span class="id" type="var">forAll</span></span> that takes a shrinker as an
    additional argument, to test properties like <span class="inlinecode"><span class="id" type="var">faultyMirrorP</span></span>. 
</div>
<div class="code code-tight">

<span class="comment">(*<br/>
&nbsp;&nbsp;QuickChick&nbsp;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(forAllShrink&nbsp;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(genTreeSized'&nbsp;5&nbsp;(choose&nbsp;(0,5)))&nbsp;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;shrink<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;faultyMirrorP).&nbsp;<br/>
*)</span><br/>
</div>

<div class="doc">
<pre>     ===&gt; 
       Node (0) (Leaf) (Node (0) (Leaf) (Leaf))

       *** Failed! After 1 tests and 8 shrinks 
</pre>

<div class="paragraph"> </div>

 We now get a quite simple counterexample (in fact, one of two
    truly minimal ones), from which it is easy to see that the bad
    behavior occurs when the subtrees of a <span class="inlinecode"><span class="id" type="var">Node</span></span> are different. 
<div class="paragraph"> </div>

<a name="lab60"></a><h2 class="section">Exercise: Ternary Trees</h2>

<div class="paragraph"> </div>

 For a comprehensive but still fairly simple exercise involving
    most of what we have seen, let's consider ternary trees, whose
    nodes have three childen instead of two. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Inductive</span> <span class="id" type="var">TernaryTree</span> <span class="id" type="var">A</span> :=<br/>
| <span class="id" type="var">TLeaf</span> : <span class="id" type="var">TernaryTree</span> <span class="id" type="var">A</span><br/>
| <span class="id" type="var">TNode</span> : <br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">A</span> → <span class="id" type="var">TernaryTree</span> <span class="id" type="var">A</span> → <span class="id" type="var">TernaryTree</span> <span class="id" type="var">A</span> → <span class="id" type="var">TernaryTree</span> <span class="id" type="var">A</span> → <span class="id" type="var">TernaryTree</span> <span class="id" type="var">A</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="var">Arguments</span> <span class="id" type="var">TLeaf</span> {<span class="id" type="var">A</span>}.<br/>
<span class="id" type="var">Arguments</span> <span class="id" type="var">TNode</span> {<span class="id" type="var">A</span>} <span class="id" type="var">_</span> <span class="id" type="var">_</span> <span class="id" type="var">_</span> <span class="id" type="var">_</span>.<br/>
</div>

<div class="doc">
Also consider the following (faulty?) mirror function. We'll want to do some
    testing to see what we can find about this function. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Fixpoint</span> <span class="id" type="var">tern_mirror</span> {<span class="id" type="var">A</span> : <span class="id" type="keyword">Type</span>} (<span class="id" type="var">t</span> : <span class="id" type="var">TernaryTree</span> <span class="id" type="var">A</span>) : <span class="id" type="var">TernaryTree</span> <span class="id" type="var">A</span> :=<br/>
&nbsp;&nbsp;<span class="id" type="keyword">match</span> <span class="id" type="var">t</span> <span class="id" type="keyword">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" type="var">TLeaf</span> ⇒ <span class="id" type="var">TLeaf</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" type="var">TNode</span> <span class="id" type="var">x</span> <span class="id" type="var">l</span> <span class="id" type="var">m</span> <span class="id" type="var">r</span> ⇒ <span class="id" type="var">TNode</span> <span class="id" type="var">x</span> (<span class="id" type="var">tern_mirror</span> <span class="id" type="var">r</span>) <span class="id" type="var">m</span> (<span class="id" type="var">tern_mirror</span> <span class="id" type="var">l</span>)<br/>
&nbsp;&nbsp;<span class="id" type="keyword">end</span>.<br/>
</div>

<div class="doc">
<a name="lab61"></a><h4 class="section">练习：1 星, standard (show_tern_tree)</h4>
 Write a <span class="inlinecode"><span class="id" type="keyword">Show</span></span> instance for Ternary Trees. 
</div>
<div class="code code-tight">

<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span><br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab62"></a><h4 class="section">练习：2 星, standard (gen_tern_tree)</h4>
 Write a generator for ternary trees. 
</div>
<div class="code code-tight">

<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span><br/>
</div>

<div class="doc">
The following line should generate a bunch of nat ternary trees. 
</div>
<div class="code code-tight">
<span class="comment">(*&nbsp;Sample&nbsp;(@genTernTreeSized&nbsp;nat&nbsp;3&nbsp;(choose&nbsp;(0,10))).&nbsp;*)</span><br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab63"></a><h4 class="section">练习：2 星, standard (shrink_tern_tree)</h4>
 Write a shrinker for ternary trees. 
</div>
<div class="code code-tight">

<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span><br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

 From the root node, we can define a path in a ternary tree by first
    defining a direction corresponding to a choice of child tree... 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Inductive</span> <span class="id" type="var">direction</span> := <span class="id" type="var">Left</span> | <span class="id" type="var">Middle</span> | <span class="id" type="var">Right</span>.<br/>
</div>

<div class="doc">
A direction tells us which child node we wish to visit. The
    <span class="inlinecode"><span class="id" type="var">traverse_node</span></span> function uses a <span class="inlinecode"><span class="id" type="var">direction</span></span> to visit the
    corresponding child. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Definition</span> <span class="id" type="var">traverse_node</span> {<span class="id" type="var">A</span>} (<span class="id" type="var">t</span>:<span class="id" type="var">direction</span>) (<span class="id" type="var">l</span> <span class="id" type="var">m</span> <span class="id" type="var">r</span>: <span class="id" type="var">TernaryTree</span> <span class="id" type="var">A</span>) :=<br/>
&nbsp;&nbsp;<span class="id" type="keyword">match</span> <span class="id" type="var">t</span> <span class="id" type="keyword">with</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">Left</span> ⇒ <span class="id" type="var">l</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">Middle</span> ⇒ <span class="id" type="var">m</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">Right</span> ⇒ <span class="id" type="var">r</span><br/>
&nbsp;&nbsp;<span class="id" type="keyword">end</span>.<br/>
</div>

<div class="doc">
A <span class="inlinecode"><span class="id" type="var">path</span></span> in a ternary tree is a list of <span class="inlinecode"><span class="id" type="var">direction</span></span>s. 
</div>
<div class="code code-tight">
<span class="id" type="keyword">Definition</span> <span class="id" type="var">path</span> := <span class="id" type="var">list</span> <span class="id" type="var">direction</span>.<br/>
</div>

<div class="doc">
We can traverse a path by iterating over the <span class="inlinecode"><span class="id" type="var">direction</span></span>s in the
    path and traversing the corresponding nodes. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Fixpoint</span> <span class="id" type="var">traverse_path</span> {<span class="id" type="var">A</span>} (<span class="id" type="var">p</span>:<span class="id" type="var">path</span>) (<span class="id" type="var">t</span>: <span class="id" type="var">TernaryTree</span> <span class="id" type="var">A</span>) :=<br/>
&nbsp;&nbsp;<span class="id" type="keyword">match</span> <span class="id" type="var">t</span> <span class="id" type="keyword">with</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">TLeaf</span> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">TLeaf</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">TNode</span> <span class="id" type="var">x</span> <span class="id" type="var">l</span> <span class="id" type="var">m</span> <span class="id" type="var">r</span> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">match</span> <span class="id" type="var">p</span> <span class="id" type="keyword">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" type="var">h</span> :: <span class="id" type="var">tl</span> ⇒ <span class="id" type="var">traverse_path</span> <span class="id" type="var">tl</span> (<span class="id" type="var">traverse_node</span> <span class="id" type="var">h</span> <span class="id" type="var">l</span> <span class="id" type="var">m</span> <span class="id" type="var">r</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;| [] ⇒ <span class="id" type="var">t</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">end</span><br/>
&nbsp;&nbsp;<span class="id" type="keyword">end</span>.<br/>
</div>

<div class="doc">
And we can mirror a path by simply swapping left and 
    right throughout. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Definition</span> <span class="id" type="var">path_mirror</span> := <span class="id" type="var">map</span> (<span class="id" type="keyword">fun</span> <span class="id" type="var">t</span> ⇒ <span class="id" type="keyword">match</span> <span class="id" type="var">t</span> <span class="id" type="keyword">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" type="var">Left</span> ⇒ <span class="id" type="var">Right</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" type="var">Right</span> ⇒ <span class="id" type="var">Left</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" type="var">_</span> ⇒ <span class="id" type="var">t</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">end</span>).<br/>
</div>

<div class="doc">
Before we can state some properties about paths in ternary trees, it's
    useful to have a decidable equality for ternary trees of <span class="inlinecode"><span class="id" type="var">nat</span></span>s. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Instance</span> <span class="id" type="var">eq_dec_tern_tree</span> (<span class="id" type="var">t<sub>1</sub></span> <span class="id" type="var">t<sub>2</sub></span> : <span class="id" type="var">TernaryTree</span> <span class="id" type="var">nat</span>) : <span class="id" type="var">Dec</span> (<span class="id" type="var">t<sub>1</sub></span> = <span class="id" type="var">t<sub>2</sub></span>) := {}.<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="var">dec_eq</span>. <span class="id" type="keyword">Defined</span>.<br/>
</div>

<div class="doc">
Traversing a path in a tree should be the same as traversing the
    mirror of the path in the mirror of the tree, just with a mirrored
    tree result. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Definition</span> <span class="id" type="var">tern_mirror_path_flip</span> (<span class="id" type="var">t</span>:<span class="id" type="var">TernaryTree</span> <span class="id" type="var">nat</span>) (<span class="id" type="var">p</span>:<span class="id" type="var">path</span>) :=<br/>
&nbsp;&nbsp;(  <span class="id" type="var">traverse_path</span> <span class="id" type="var">p</span> <span class="id" type="var">t</span> <br/>
&nbsp;&nbsp;&nbsp;= <span class="id" type="var">tern_mirror</span> (<span class="id" type="var">traverse_path</span> (<span class="id" type="var">path_mirror</span> <span class="id" type="var">p</span>) (<span class="id" type="var">tern_mirror</span> <span class="id" type="var">t</span>))) ?.<br/>
</div>

<div class="doc">
Before using this property to test <span class="inlinecode"><span class="id" type="var">tern_mirror</span></span>, we'll need to be
    able to generate, show, and shrink paths. To start, we'll derive
    those For <span class="inlinecode"><span class="id" type="var">directions</span></span>. The <span class="inlinecode"><span class="id" type="keyword">Show</span></span> and <span class="inlinecode"><span class="id" type="var">G</span></span> definitions for
    <span class="inlinecode"><span class="id" type="var">direction</span></span> are simple to write; the <span class="inlinecode"><span class="id" type="var">shrink</span></span> will by default go
    left. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Instance</span> <span class="id" type="var">showDirection</span> : <span class="id" type="keyword">Show</span> <span class="id" type="var">direction</span> :=<br/>
&nbsp;&nbsp;{| <span class="id" type="var">show</span> <span class="id" type="var">x</span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">match</span> <span class="id" type="var">x</span> <span class="id" type="keyword">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" type="var">Left</span> ⇒ "Left"<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" type="var">Middle</span> ⇒ "Middle"<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" type="var">Right</span> ⇒ "Right"<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">end</span> |}.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">genDirection</span> : <span class="id" type="var">G</span> <span class="id" type="var">direction</span> :=<br/>
&nbsp;&nbsp;<span class="id" type="var">elems</span> [<span class="id" type="var">Left</span>; <span class="id" type="var">Middle</span>; <span class="id" type="var">Right</span>].<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Instance</span> <span class="id" type="var">shrinkDirection</span> : <span class="id" type="var">Shrink</span> <span class="id" type="var">direction</span> :=<br/>
&nbsp;&nbsp;{| <span class="id" type="var">shrink</span> <span class="id" type="var">d</span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">match</span> <span class="id" type="var">d</span> <span class="id" type="keyword">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" type="var">Left</span> ⇒ []<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" type="var">Right</span> | <span class="id" type="var">Middle</span> ⇒ [<span class="id" type="var">Left</span>]<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">end</span> |}.<br/>
</div>

<div class="doc">
For generating a list of paths, we'll use the built-in function
    <span class="inlinecode"><span class="id" type="var">listOf</span></span>, which takes a generator for a type and generates lists
    of elements of that type.  We do the same for <span class="inlinecode"><span class="id" type="var">show</span></span> and <span class="inlinecode"><span class="id" type="var">shrink</span></span>
    with <span class="inlinecode"><span class="id" type="var">showList</span></span> and <span class="inlinecode"><span class="id" type="var">shrinkList</span></span> respectively. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Instance</span> <span class="id" type="var">showPath</span> : <span class="id" type="keyword">Show</span> <span class="id" type="var">path</span> := <span class="id" type="var">showList</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">genPath</span> : <span class="id" type="var">G</span> <span class="id" type="var">path</span> :=<br/>
&nbsp;&nbsp;<span class="id" type="var">listOf</span> <span class="id" type="var">genDirection</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Instance</span> <span class="id" type="var">shrinkPath</span> : <span class="id" type="var">Shrink</span> <span class="id" type="var">path</span> := <span class="id" type="var">shrinkList</span>.<br/>
</div>

<div class="doc">
<a name="lab64"></a><h4 class="section">练习：4 星, standard (bug_finding_tern_tree)</h4>
 Using <span class="inlinecode"><span class="id" type="var">genTernTreeSized</span></span> and <span class="inlinecode"><span class="id" type="var">shrinkTernTree</span></span> find (and fix!) any
    bugs in <span class="inlinecode"><span class="id" type="var">tern_mirror</span></span>. 
</div>
<div class="code code-tight">

<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span><br/>
</div>

<span class="proofbox">&#9744;</span> 

<div class="doc">
<a name="lab65"></a><h1 class="section">Putting it all Together</h1>

<div class="paragraph"> </div>

 Now we've got pretty much all the basic machinery we need, but the
    way we write properties &mdash; using <span class="inlinecode"><span class="id" type="var">forAllShrink</span></span> and explicitly
    providing generators and shrinkers &mdash; is still heavier than it
    needs to be.  We can use a bit more typeclass magic to further
    lighten things.

<div class="paragraph"> </div>

    First, we introduce a typeclass <span class="inlinecode"><span class="id" type="var">Gen</span></span> <span class="inlinecode"><span class="id" type="var">A</span></span> with a single operator
    <span class="inlinecode"><span class="id" type="var">arbitrary</span></span> of type <span class="inlinecode"><span class="id" type="var">G</span></span> <span class="inlinecode"><span class="id" type="var">A</span></span>. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Module</span> <span class="id" type="var">DefineGen</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Class</span> <span class="id" type="var">Gen</span> (<span class="id" type="var">A</span> : <span class="id" type="keyword">Type</span>) :=<br/>
&nbsp;&nbsp;{<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">arbitrary</span> : <span class="id" type="var">G</span> <span class="id" type="var">A</span><br/>
&nbsp;&nbsp;}.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">End</span> <span class="id" type="var">DefineGen</span>.<br/>
</div>

<div class="doc">
Intuitively, <span class="inlinecode"><span class="id" type="var">Gen</span></span> is a way of uniformly packaging up the
    generators for various types so that we do not need to remember
    their individual names &mdash; we can just call them all
    <span class="inlinecode"><span class="id" type="var">arbitrary</span></span>. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Instance</span> <span class="id" type="var">gen_color</span> : <span class="id" type="var">Gen</span> <span class="id" type="var">color</span> :=<br/>
&nbsp;&nbsp;{<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">arbitrary</span> := <span class="id" type="var">genColor</span><br/>
&nbsp;&nbsp;}.<br/>
</div>

<div class="doc">
Next, for convenience we package <span class="inlinecode"><span class="id" type="var">Gen</span></span> and <span class="inlinecode"><span class="id" type="var">Shrink</span></span> together into
    an <span class="inlinecode"><span class="id" type="var">Arbitrary</span></span> typeclass that is a subclass of both. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Module</span> <span class="id" type="var">DefineArbitrary</span>.<br/>
<span class="id" type="keyword">Import</span> <span class="id" type="var">DefineGen</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Class</span> <span class="id" type="var">Arbitrary</span> (<span class="id" type="var">A</span> : <span class="id" type="keyword">Type</span>) `{<span class="id" type="var">Gen</span> <span class="id" type="var">A</span>} `{<span class="id" type="var">Shrink</span> <span class="id" type="var">A</span>}.<br/>
</div>

<div class="doc">
(The empty "body" of <span class="inlinecode"><span class="id" type="var">Arbitrary</span></span> is elided.) 
</div>
<div class="code code-tight">

<span class="id" type="keyword">End</span> <span class="id" type="var">DefineArbitrary</span>.<br/>
</div>

<div class="doc">
We can use the top-level <span class="inlinecode"><span class="id" type="var">QuickChick</span></span> command on quantified
    propositions with generatable and decidable conclusions, stating
    just the property and letting the typeclass machinery figure out
    the rest.  

<div class="paragraph"> </div>

    For example, suppose we want to test this: 
</div>
<div class="code code-tight">

<span class="id" type="var">Conjecture</span> <span class="id" type="var">every_color_is_red</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">c</span>, <span class="id" type="var">c</span> = <span class="id" type="var">Red</span>.<br/>
</div>

<div class="doc">
Since we have already defined <span class="inlinecode"><span class="id" type="var">Gen</span></span> and <span class="inlinecode"><span class="id" type="var">Shrink</span></span> instances for
    <span class="inlinecode"><span class="id" type="var">color</span></span>, we automatically get an <span class="inlinecode"><span class="id" type="var">Arbitrary</span></span> instance.  The <span class="inlinecode"><span class="id" type="var">Gen</span></span>
    part is used by the checker instance for "forall" propositions to
    generate random <span class="inlinecode"><span class="id" type="var">color</span></span> arguments.

<div class="paragraph"> </div>

    To show that the conclusion is decidable, we need to define a
    <span class="inlinecode"><span class="id" type="var">Dec</span></span> instance for equality on colors. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Instance</span> <span class="id" type="var">eq_dec_color</span> (<span class="id" type="var">x</span> <span class="id" type="var">y</span> : <span class="id" type="var">color</span>) : <span class="id" type="var">Dec</span> (<span class="id" type="var">x</span> = <span class="id" type="var">y</span>).<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="var">dec_eq</span>. <span class="id" type="keyword">Defined</span>.<br/>
</div>

<div class="doc">
Putting it all together: 
</div>
<div class="code code-tight">

<span class="comment">(*&nbsp;&nbsp;QuickChick&nbsp;every_color_is_red.&nbsp;*)</span><br/>
</div>

<div class="doc">
<pre>     ===&gt;
       QuickChecking every_color_is_red
       Green
       *** Failed after 1 tests and 1 shrinks. (0 discards) 
</pre>

</div>

<div class="doc">
<a name="lab66"></a><h1 class="section">Sized Generators</h1>

<div class="paragraph"> </div>

 Suppose we want to build an <span class="inlinecode"><span class="id" type="var">Arbitrary</span></span> instance for trees.

<div class="paragraph"> </div>

    We would like to use <span class="inlinecode"><span class="id" type="var">genTreeSized'</span></span>; however, that generator
    takes an additional <span class="inlinecode"><span class="id" type="var">size</span></span> argument.

<div class="paragraph"> </div>

    Fortunately, since the <span class="inlinecode"><span class="id" type="var">G</span></span> monad itself includes a size argument,
    we can "plumb" this argument into generators like <span class="inlinecode"><span class="id" type="var">genTreeSized'</span></span>.

<div class="paragraph"> </div>

    In other words, we can define an operator <span class="inlinecode"><span class="id" type="var">sized</span></span> that takes a
]    sized generator and produces an unsized one. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Module</span> <span class="id" type="var">DefineSized</span>.<br/>
<span class="id" type="keyword">Import</span> <span class="id" type="var">DefineG</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">sized</span> {<span class="id" type="var">A</span> : <span class="id" type="keyword">Type</span>} (<span class="id" type="var">f</span> : <span class="id" type="var">nat</span> → <span class="id" type="var">G</span> <span class="id" type="var">A</span>) : <span class="id" type="var">G</span> <span class="id" type="var">A</span> :=<br/>
&nbsp;&nbsp;<span class="id" type="var">MkG</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="keyword">fun</span> <span class="id" type="var">n</span> <span class="id" type="var">r</span> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">match</span> <span class="id" type="var">f</span> <span class="id" type="var">n</span> <span class="id" type="keyword">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">MkG</span> <span class="id" type="var">g</span> ⇒ <span class="id" type="var">g</span> <span class="id" type="var">n</span> <span class="id" type="var">r</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">end</span>).<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">End</span> <span class="id" type="var">DefineSized</span>.<br/>
</div>

<div class="doc">
To streamline assembling generators, it is convenient to introduce
    one more typeclass, <span class="inlinecode"><span class="id" type="var">GenSized</span></span>, whose instances are sized
    generators. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Module</span> <span class="id" type="var">DefineGenSized</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Class</span> <span class="id" type="var">GenSized</span> (<span class="id" type="var">A</span> : <span class="id" type="keyword">Type</span>) :=<br/>
&nbsp;&nbsp;{<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">arbitrarySized</span> : <span class="id" type="var">nat</span> → <span class="id" type="var">G</span> <span class="id" type="var">A</span><br/>
&nbsp;&nbsp;}.<br/>
</div>

<div class="doc">
We can then define a generic <span class="inlinecode"><span class="id" type="var">Gen</span></span> instance for types that have a
    <span class="inlinecode"><span class="id" type="var">GenSized</span></span> instance, using <span class="inlinecode"><span class="id" type="var">sized</span></span>: 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Instance</span> <span class="id" type="var">GenOfGenSized</span> {<span class="id" type="var">A</span>} `{<span class="id" type="var">GenSized</span> <span class="id" type="var">A</span>} : <span class="id" type="var">Gen</span> <span class="id" type="var">A</span> :=<br/>
&nbsp;&nbsp;{<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">arbitrary</span> := <span class="id" type="var">sized</span> <span class="id" type="var">arbitrarySized</span><br/>
&nbsp;&nbsp;}.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">End</span> <span class="id" type="var">DefineGenSized</span>.<br/>
</div>

<div class="doc">
Now we can make a <span class="inlinecode"><span class="id" type="var">Gen</span></span> instance for trees by providing just an
    implementation of <span class="inlinecode"><span class="id" type="var">arbitrarySized</span></span>. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Instance</span> <span class="id" type="var">genTree</span> {<span class="id" type="var">A</span>} `{<span class="id" type="var">Gen</span> <span class="id" type="var">A</span>} : <span class="id" type="var">GenSized</span> (<span class="id" type="var">Tree</span> <span class="id" type="var">A</span>) := <br/>
&nbsp;&nbsp;{| <span class="id" type="var">arbitrarySized</span> <span class="id" type="var">n</span> := <span class="id" type="var">genTreeSized'</span> <span class="id" type="var">n</span> <span class="id" type="var">arbitrary</span> |}.<br/>
</div>

<div class="doc">
Finally, with the <span class="inlinecode"><span class="id" type="var">Arbitrary</span></span> instance for trees, we can supply
    just <span class="inlinecode"><span class="id" type="var">faultyMirrorP</span></span> to the <span class="inlinecode"><span class="id" type="var">QuickChick</span></span> command. 
</div>
<div class="code code-tight">

<span class="comment">(*&nbsp;QuickChick&nbsp;faultyMirrorP.&nbsp;*)</span><br/>
</div>

<div class="doc">
<a name="lab67"></a><h4 class="section">练习：2 星, standard (tern_tree_typeclasses)</h4>
 Add typeclass instances for <span class="inlinecode"><span class="id" type="var">GenSized</span></span> and <span class="inlinecode"><span class="id" type="var">Shrink</span></span> so that you
    can <span class="inlinecode"><span class="id" type="var">QuickChick</span></span> <span class="inlinecode"><span class="id" type="var">tern_mirror_reverse</span></span> directly. 
</div>
<div class="code code-tight">

<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span><br/><hr class='doublespaceincode'/>
<span class="comment">(*&nbsp;QuickChick&nbsp;tern_mirror_reverse.&nbsp;*)</span><br/>
</div>

<span class="proofbox">&#9744;</span> 

<div class="doc">
<a name="lab68"></a><h1 class="section">Automation</h1>

<div class="paragraph"> </div>

 Writing <span class="inlinecode"><span class="id" type="keyword">Show</span></span> and <span class="inlinecode"><span class="id" type="var">Arbitrary</span></span> instances is usually not hard, but
    it can get tedious when we are testing code that involves many new
    <span class="inlinecode"><span class="id" type="keyword">Inductive</span></span> type declarations.  To streamline this process,
    <span class="inlinecode"><span class="id" type="var">QuickChick</span></span> provides some automation for deriving such instances
    for "plain datatypes" automatically! 
</div>
<div class="code code-tight">

<span class="id" type="var">Derive</span> <span class="id" type="var">Arbitrary</span> <span class="id" type="keyword">for</span> <span class="id" type="var">Tree</span>.<br/>
</div>

<div class="doc">
<pre>     ===&gt; GenSizedree is defined 
     ===&gt; ShrinkTree is defined 
</pre>

</div>
<div class="code code-tight">
<span class="id" type="keyword">Print</span> <span class="id" type="var">GenSizedTree</span>.<br/>
<span class="id" type="keyword">Print</span> <span class="id" type="var">ShrinkTree</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="var">Derive</span> <span class="id" type="keyword">Show</span> <span class="id" type="keyword">for</span> <span class="id" type="var">Tree</span>.<br/>
</div>

<div class="doc">

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;===&gt;&nbsp;<span class="id" type="var">ShowTree</span>&nbsp;<span class="id" type="var">is</span>&nbsp;<span class="id" type="var">defined</span>&nbsp;
<div class="paragraph"> </div>

</div>

</div>
<div class="code code-tight">
<span class="id" type="keyword">Print</span> <span class="id" type="var">ShowTree</span>.<br/>
</div>

<div class="doc">
<a name="lab69"></a><h1 class="section">Collecting Statistics</h1>

<div class="paragraph"> </div>

 Earlier in this tutorial we observed that our first definition of
    <span class="inlinecode"><span class="id" type="var">genTreeSized</span></span> seemed to be producing too many <span class="inlinecode"><span class="id" type="var">Leaf</span></span>
    constructors.

<div class="paragraph"> </div>

    In that case, just eyeballing at a few results from <span class="inlinecode"><span class="id" type="var">Sample</span></span> gave
    us an idea that something was wrong with the distribution of test
    cases, but it's often useful to collect more extensive statistics
    from larger sets of samples.

<div class="paragraph"> </div>

    This is where <span class="inlinecode"><span class="id" type="var">collect</span></span>, another property combinator, comes in. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Check</span> @<span class="id" type="var">collect</span>.<br/>
</div>

<div class="doc">

<div class="paragraph"> </div>

<pre>     ===&gt; 
     @collect
       : forall A prop : Type, Show A <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> Checkable prop <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> 
           A <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> prop <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> Checker
</pre>

<div class="paragraph"> </div>

 That is, <span class="inlinecode"><span class="id" type="var">collect</span></span> takes a checkable proposition and returns a new
    <span class="inlinecode"><span class="id" type="var">Checker</span></span> (for the same proposition).

<div class="paragraph"> </div>

    On the side, it takes a value from some <span class="inlinecode"><span class="id" type="keyword">Show</span></span>able type <span class="inlinecode"><span class="id" type="var">A</span></span>, which
    it remembers internally (in an enriched variant of the <span class="inlinecode"><span class="id" type="var">Result</span></span>
    structure that we saw above) so that it can be collated and
    displayed at the end. 
<div class="paragraph"> </div>

 For example, suppose we measure the <span class="inlinecode"><span class="id" type="var">size</span></span> of <span class="inlinecode"><span class="id" type="var">Tree</span></span>s like this: 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Fixpoint</span> <span class="id" type="var">size</span> {<span class="id" type="var">A</span>} (<span class="id" type="var">t</span> : <span class="id" type="var">Tree</span> <span class="id" type="var">A</span>) : <span class="id" type="var">nat</span> :=<br/>
&nbsp;&nbsp;<span class="id" type="keyword">match</span> <span class="id" type="var">t</span> <span class="id" type="keyword">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" type="var">Leaf</span> ⇒ <span class="id" type="var">O</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" type="var">Node</span> <span class="id" type="var">_</span> <span class="id" type="var">l</span> <span class="id" type="var">r</span> ⇒ 1 + <span class="id" type="var">size</span> <span class="id" type="var">l</span> + <span class="id" type="var">size</span> <span class="id" type="var">r</span><br/>
&nbsp;&nbsp;<span class="id" type="keyword">end</span>.<br/>
</div>

<div class="doc">
We can write a dummy property <span class="inlinecode"><span class="id" type="var">treeProp</span></span> to collect the sizes of
    the trees we are generating. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Definition</span> <span class="id" type="var">treeProp</span> (<span class="id" type="var">g</span> : <span class="id" type="var">nat</span> → <span class="id" type="var">G</span> <span class="id" type="var">nat</span> → <span class="id" type="var">G</span> (<span class="id" type="var">Tree</span> <span class="id" type="var">nat</span>)) <span class="id" type="var">n</span> :=<br/>
&nbsp;&nbsp;<span class="id" type="var">forAll</span> (<span class="id" type="var">g</span> <span class="id" type="var">n</span> (<span class="id" type="var">choose</span> (0,<span class="id" type="var">n</span>))) (<span class="id" type="keyword">fun</span> <span class="id" type="var">t</span> ⇒ <span class="id" type="var">collect</span> (<span class="id" type="var">size</span> <span class="id" type="var">t</span>) <span class="id" type="var">true</span>).<br/><hr class='doublespaceincode'/>
<span class="comment">(*&nbsp;QuickChick&nbsp;(treeProp&nbsp;genTreeSized&nbsp;5).&nbsp;*)</span><br/>
</div>

<div class="doc">
<pre>     ===&gt; 
       4947 : 0
       1258 : 1
       673 : 2
       464 : 6
       427 : 5
       393 : 3
       361 : 7
       302 : 4
       296 : 8
       220 : 9
       181 : 10
       127 : 11
       104 : 12
       83 : 13
       64 : 14
       32 : 15
       25 : 16
       16 : 17
       13 : 18
       6 : 19
       5 : 20
       2 : 21
       1 : 23

       +++ OK, passed 10000 tests 
</pre>

<div class="paragraph"> </div>

 We see that 62.5% of the tests (4947 + 1258 / 10000) are either
    <span class="inlinecode"><span class="id" type="var">Leaf</span></span>s or empty <span class="inlinecode"><span class="id" type="var">Node</span></span>s, while rather few tests have larger
    sizes.  
<div class="paragraph"> </div>

 Compare this with <span class="inlinecode"><span class="id" type="var">genTreeSized'</span></span>.  
</div>
<div class="code code-tight">

<span class="comment">(*&nbsp;QuickChick&nbsp;(treeProp&nbsp;genTreeSized'&nbsp;5).&nbsp;*)</span><br/>
</div>

<div class="doc">
<pre>     ===&gt; 
       1624 : 0
       571 : 10
       564 : 12
       562 : 11
       559 : 9
       545 : 8
       539 : 14
       534 : 13
       487 : 7
       487 : 15
       437 : 16
       413 : 6
       390 : 17
       337 : 5
       334 : 1
       332 : 18
       286 : 19
       185 : 4
       179 : 20
       179 : 2
       138 : 21
       132 : 3 
       87 : 22
       62 : 23
       19 : 24
       10 : 25
       6 : 26
       2 : 27

       +++ OK, passed 10000 tests 
</pre>

<div class="paragraph"> </div>

 This generates far fewer tiny examples, likely leading to more
    efficient testing of interesting properties. 
</div>

<div class="doc">
<a name="lab70"></a><h1 class="section">Dealing with Preconditions</h1>

<div class="paragraph"> </div>

 A large class of properties that are commonly encountered in
    property-based testing are _properties with preconditions_.  The
    default QuickChick approach of generating inputs based on type
    information can be inefficient for such properties, especially for
    those with sparse preconditions (i.e. ones that are satisfied
    rarely with respect to their input domain). 
</div>

<div class="doc">
Consider a function that inserts a natural number into a sorted list. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Fixpoint</span> <span class="id" type="var">sorted</span> (<span class="id" type="var">l</span> : <span class="id" type="var">list</span> <span class="id" type="var">nat</span>) := <br/>
&nbsp;&nbsp;<span class="id" type="keyword">match</span> <span class="id" type="var">l</span> <span class="id" type="keyword">with</span> <br/>
&nbsp;&nbsp;| [] ⇒ <span class="id" type="var">true</span> <br/>
&nbsp;&nbsp;| <span class="id" type="var">x</span>::<span class="id" type="var">xs</span> ⇒ <span class="id" type="keyword">match</span> <span class="id" type="var">xs</span> <span class="id" type="keyword">with</span> <br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| [] ⇒ <span class="id" type="var">true</span> <br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" type="var">y</span> :: <span class="id" type="var">ys</span> ⇒ (<span class="id" type="var">x</span> &lt;=? <span class="id" type="var">y</span>) &amp;&amp; (<span class="id" type="var">sorted</span> <span class="id" type="var">xs</span>) <br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">end</span> <br/>
&nbsp;&nbsp;<span class="id" type="keyword">end</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Fixpoint</span> <span class="id" type="var">insert</span> (<span class="id" type="var">x</span> : <span class="id" type="var">nat</span>) (<span class="id" type="var">l</span> : <span class="id" type="var">list</span> <span class="id" type="var">nat</span>) := <br/>
&nbsp;&nbsp;<span class="id" type="keyword">match</span> <span class="id" type="var">l</span> <span class="id" type="keyword">with</span> <br/>
&nbsp;&nbsp;| [] ⇒ [<span class="id" type="var">x</span>] <br/>
&nbsp;&nbsp;| <span class="id" type="var">y</span>::<span class="id" type="var">ys</span> ⇒ <span class="id" type="keyword">if</span> <span class="id" type="var">x</span> &lt;=? <span class="id" type="var">y</span> <span class="id" type="keyword">then</span> <span class="id" type="var">x</span> :: <span class="id" type="var">l</span> <br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">else</span> <span class="id" type="var">y</span> :: <span class="id" type="var">insert</span> <span class="id" type="var">x</span> <span class="id" type="var">ys</span> <br/>
&nbsp;&nbsp;<span class="id" type="keyword">end</span>.<br/>
</div>

<div class="doc">
We could test <span class="inlinecode"><span class="id" type="var">insert</span></span> using the following _conditional_ property: 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Definition</span> <span class="id" type="var">insert_spec</span> (<span class="id" type="var">x</span> : <span class="id" type="var">nat</span>) (<span class="id" type="var">l</span> : <span class="id" type="var">list</span> <span class="id" type="var">nat</span>) :=<br/>
&nbsp;&nbsp;<span class="id" type="var">sorted</span> <span class="id" type="var">l</span> ==&gt; <span class="id" type="var">sorted</span> (<span class="id" type="var">insert</span> <span class="id" type="var">x</span> <span class="id" type="var">l</span>).<br/><hr class='doublespaceincode'/>
<span class="comment">(*&nbsp;QuickChick&nbsp;insert_spec.&nbsp;*)</span><br/>
</div>

<div class="doc">
<pre>     ===&gt; 
       QuickChecking insert_spec 
       +++ Passed 10000 tests (17325 discards) 
</pre>

<div class="paragraph"> </div>

 To test this property, QuickChick will try to generate random
    integers <span class="inlinecode"><span class="id" type="var">x</span></span> and lists <span class="inlinecode"><span class="id" type="var">l</span></span>, _check_ whether the generated <span class="inlinecode"><span class="id" type="var">l</span></span> is
    sorted, and, if it is, proceed to check the conclusion. If it is
    not, it will discard the generated inputs and try again.

<div class="paragraph"> </div>

    As we can see, this can lead to many discarded tests (in this
    case, about twice as many as successful ones), which wastes a
    lot of CPU and leads to inefficient testing. 
<div class="paragraph"> </div>

 But the wasted effort is the least of our problems! Let's take a
    peek at the distribution of the lengths of generated lists using
    <span class="inlinecode"><span class="id" type="var">collect</span></span>. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Definition</span> <span class="id" type="var">insert_spec'</span> (<span class="id" type="var">x</span> : <span class="id" type="var">nat</span>) (<span class="id" type="var">l</span> : <span class="id" type="var">list</span> <span class="id" type="var">nat</span>) :=<br/>
&nbsp;&nbsp;<span class="id" type="var">collect</span> (<span class="id" type="var">List.length</span> <span class="id" type="var">l</span>) (<span class="id" type="var">insert_spec</span> <span class="id" type="var">x</span> <span class="id" type="var">l</span>).<br/><hr class='doublespaceincode'/>
<span class="comment">(*&nbsp;QuickChick&nbsp;insert_spec'.&nbsp;*)</span><br/>
</div>

<div class="doc">
<pre>     ===&gt; 
   QuickChecking insert_spec' 
   3447 : 0 
   3446 : 1 
   1929 : 2 
   788 : 3 
   271 : 4 
   96 : 5 
   19 : 6 
   4 : 7 
   +++ Passed 10000 tests (17263 discards) 
</pre>
 The vast majority of inputs have length 2 or less!

<div class="paragraph"> </div>

    (This explains something you might have found suspicious in the
    previous statistics: that 1/3 of the randomly generated lists were
    already sorted!) 
<div class="paragraph"> </div>

 When dealing with properties with preconditions, it is common
    practice to write custom generators for well-distributed random
    data that satisfy the property. 
<div class="paragraph"> </div>

 For example, we can generate sorted lists with elements between
    <span class="inlinecode"><span class="id" type="var">low</span></span> and <span class="inlinecode"><span class="id" type="var">high</span></span> like this... 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Fixpoint</span> <span class="id" type="var">genSortedList</span> (<span class="id" type="var">low</span> <span class="id" type="var">high</span> : <span class="id" type="var">nat</span>) (<span class="id" type="var">size</span> : <span class="id" type="var">nat</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;: <span class="id" type="var">G</span> (<span class="id" type="var">list</span> <span class="id" type="var">nat</span>) :=<br/>
&nbsp;&nbsp;<span class="id" type="keyword">match</span> <span class="id" type="var">size</span> <span class="id" type="keyword">with</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">O</span> ⇒ <span class="id" type="var">ret</span> []<br/>
&nbsp;&nbsp;| <span class="id" type="var">S</span> <span class="id" type="var">size'</span> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">if</span> <span class="id" type="var">high</span> &lt;? <span class="id" type="var">low</span> <span class="id" type="keyword">then</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">ret</span> []<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">else</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">freq</span> [ (1, <span class="id" type="var">ret</span> []) ;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">size</span>, <span class="id" type="var">x</span> &lt;- <span class="id" type="var">choose</span> (<span class="id" type="var">low</span>, <span class="id" type="var">high</span>);;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">xs</span> &lt;- <span class="id" type="var">genSortedList</span> <span class="id" type="var">x</span> <span class="id" type="var">high</span> <span class="id" type="var">size'</span>;; <br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">ret</span> (<span class="id" type="var">x</span> :: <span class="id" type="var">xs</span>)) ] <span class="id" type="keyword">end</span>.<br/>
</div>

<div class="doc">
We use a <span class="inlinecode"><span class="id" type="var">size</span></span> parameter as usual to control the length of generated
    lists. 
<div class="paragraph"> </div>

 If <span class="inlinecode"><span class="id" type="var">size</span></span> is zero, we can only return the empty list which
    is always sorted. If <span class="inlinecode"><span class="id" type="var">size</span></span> is nonzero, we need to perform an
    additional check whether <span class="inlinecode"><span class="id" type="var">high</span></span> is less than <span class="inlinecode"><span class="id" type="var">low</span></span> (in which case
    we also return the empty list).  If it is not, we can proceed to
    choose to generate a cons cell, with its head generated between
    <span class="inlinecode"><span class="id" type="var">low</span></span> and <span class="inlinecode"><span class="id" type="var">high</span></span> and its tail generated recursively. 
</div>
<div class="code code-tight">

<span class="comment">(*&nbsp;Sample&nbsp;(genSortedList&nbsp;0&nbsp;10&nbsp;10).&nbsp;*)</span><br/>
</div>

<div class="doc">
Finally, we can use <span class="inlinecode"><span class="id" type="var">forAllShrink</span></span> to define a property using the
    new generator: 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Definition</span> <span class="id" type="var">insert_spec_sorted</span> (<span class="id" type="var">x</span> : <span class="id" type="var">nat</span>) :=<br/>
&nbsp;&nbsp;<span class="id" type="var">forAllShrink</span> <br/>
&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">genSortedList</span> 0 10 10) <br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">shrink</span> <br/>
&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="keyword">fun</span> <span class="id" type="var">l</span> ⇒ <span class="id" type="var">insert_spec'</span> <span class="id" type="var">x</span> <span class="id" type="var">l</span>).<br/>
</div>

<div class="doc">
Now the distribution of lengths looks much better, and we don't
    discard any tests! 
</div>
<div class="code code-tight">

<span class="id" type="var">QuickChick</span> <span class="id" type="var">insert_spec_sorted</span>.<br/>
</div>

<div class="doc">
<pre>     ===&gt;
       QuickChecking insert_spec_sorted
       947 : 0
       946 : 4
       946 : 10
       938 : 6
       922 : 9
       916 : 2
       900 : 7
       899 : 3
       885 : 8
       854 : 5
       847 : 1
       +++ Passed 10000 tests (0 discards) 
</pre>
 Does this mean we are happy? 
<div class="paragraph"> </div>

<a name="lab71"></a><h4 class="section">练习：5 星, standard, optional (uniform_sorted)</h4>
 Using "collect", find out whether generating a sorted list of
    numbers between 0 and 5 is uniform in the frequencies with which
    different _numbers_ are found in the generated lists.

<div class="paragraph"> </div>

    If not, figure out why.  Then write a different generator that
    achieves a more uniform distribution (preserving uniformity in the
    lengths). 
</div>
<div class="code code-tight">

<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span><br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab72"></a><h2 class="section">Another Precondition: Binary Search Trees</h2>

<div class="paragraph"> </div>

 To conclude this chapter, let's look at _binary search trees_.

<div class="paragraph"> </div>

    The <span class="inlinecode"><span class="id" type="var">isBST</span></span> predicate characterizes trees with elements between
    <span class="inlinecode"><span class="id" type="var">low</span></span> and <span class="inlinecode"><span class="id" type="var">high</span></span>. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Fixpoint</span> <span class="id" type="var">isBST</span> (<span class="id" type="var">low</span> <span class="id" type="var">high</span>: <span class="id" type="var">nat</span>) (<span class="id" type="var">t</span> : <span class="id" type="var">Tree</span> <span class="id" type="var">nat</span>) := <br/>
&nbsp;&nbsp;<span class="id" type="keyword">match</span> <span class="id" type="var">t</span> <span class="id" type="keyword">with</span> <br/>
&nbsp;&nbsp;| <span class="id" type="var">Leaf</span> ⇒ <span class="id" type="var">true</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">Node</span> <span class="id" type="var">x</span> <span class="id" type="var">l</span> <span class="id" type="var">r</span> ⇒ (<span class="id" type="var">low</span> &lt;? <span class="id" type="var">x</span>) &amp;&amp; (<span class="id" type="var">x</span> &lt;? <span class="id" type="var">high</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&amp;&amp; (<span class="id" type="var">isBST</span> <span class="id" type="var">low</span> <span class="id" type="var">x</span> <span class="id" type="var">l</span>) &amp;&amp; (<span class="id" type="var">isBST</span> <span class="id" type="var">x</span> <span class="id" type="var">high</span> <span class="id" type="var">r</span>)<br/>
&nbsp;&nbsp;<span class="id" type="keyword">end</span>.<br/>
</div>

<div class="doc">
Here is a (faulty?) insertion function for binary search trees. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Fixpoint</span> <span class="id" type="var">insertBST</span> (<span class="id" type="var">x</span> : <span class="id" type="var">nat</span>) (<span class="id" type="var">t</span> : <span class="id" type="var">Tree</span> <span class="id" type="var">nat</span>) :=<br/>
&nbsp;&nbsp;<span class="id" type="keyword">match</span> <span class="id" type="var">t</span> <span class="id" type="keyword">with</span> <br/>
&nbsp;&nbsp;| <span class="id" type="var">Leaf</span> ⇒ <span class="id" type="var">Node</span> <span class="id" type="var">x</span> <span class="id" type="var">Leaf</span> <span class="id" type="var">Leaf</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">Node</span> <span class="id" type="var">x'</span> <span class="id" type="var">l</span> <span class="id" type="var">r</span> ⇒ <span class="id" type="keyword">if</span> <span class="id" type="var">x</span> &lt;? <span class="id" type="var">x'</span> <span class="id" type="keyword">then</span> <span class="id" type="var">Node</span> <span class="id" type="var">x'</span> (<span class="id" type="var">insertBST</span> <span class="id" type="var">x</span> <span class="id" type="var">l</span>) <span class="id" type="var">r</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">else</span> <span class="id" type="var">Node</span> <span class="id" type="var">x'</span> <span class="id" type="var">l</span> (<span class="id" type="var">insertBST</span> <span class="id" type="var">x</span> <span class="id" type="var">r</span>)<br/>
&nbsp;&nbsp;<span class="id" type="keyword">end</span>.<br/>
</div>

<div class="doc">
We would expect that if we insert an element that is within 
    the bounds <span class="inlinecode"><span class="id" type="var">low</span></span> and <span class="inlinecode"><span class="id" type="var">high</span></span> into a binary search tree, then
    the result is also a binary search tree. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Definition</span> <span class="id" type="var">insertBST_spec</span> (<span class="id" type="var">low</span> <span class="id" type="var">high</span> : <span class="id" type="var">nat</span>) (<span class="id" type="var">x</span> : <span class="id" type="var">nat</span>) (<span class="id" type="var">t</span> : <span class="id" type="var">Tree</span> <span class="id" type="var">nat</span>) :=<br/>
&nbsp;&nbsp;(<span class="id" type="var">low</span> &lt;? <span class="id" type="var">x</span>) ==&gt; <br/>
&nbsp;&nbsp;(<span class="id" type="var">x</span> &lt;? <span class="id" type="var">high</span>) ==&gt; <br/>
&nbsp;&nbsp;(<span class="id" type="var">isBST</span> <span class="id" type="var">low</span> <span class="id" type="var">high</span> <span class="id" type="var">t</span>) ==&gt; <br/>
&nbsp;&nbsp;<span class="id" type="var">isBST</span> <span class="id" type="var">low</span> <span class="id" type="var">high</span> (<span class="id" type="var">insertBST</span> <span class="id" type="var">x</span> <span class="id" type="var">t</span>).<br/><hr class='doublespaceincode'/>
<span class="comment">(*&nbsp;QuickChick&nbsp;insertBST_spec.&nbsp;*)</span><br/>
</div>

<div class="doc">

<div class="paragraph"> </div>

<pre>
    ===&gt; 
      QuickChecking insertBST_spec
      0
      5
      4
      Node (4) (Leaf) (Leaf)
      *** Failed after 85 tests and 1 shrinks. (1274 discards) 
</pre>

<div class="paragraph"> </div>

 We can see that a bug exists when inserting an element into a
    <span class="inlinecode"><span class="id" type="var">Node</span></span> with the same payload: if the element already exists in the
    binary search tree, we should not change it. 
<div class="paragraph"> </div>

 However we are wasting too much testing effort.  Indeed, if we fix the
    bug ... 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Fixpoint</span> <span class="id" type="var">insertBST'</span> (<span class="id" type="var">x</span> : <span class="id" type="var">nat</span>) (<span class="id" type="var">t</span> : <span class="id" type="var">Tree</span> <span class="id" type="var">nat</span>) :=<br/>
&nbsp;&nbsp;<span class="id" type="keyword">match</span> <span class="id" type="var">t</span> <span class="id" type="keyword">with</span> <br/>
&nbsp;&nbsp;| <span class="id" type="var">Leaf</span> ⇒ <span class="id" type="var">Node</span> <span class="id" type="var">x</span> <span class="id" type="var">Leaf</span> <span class="id" type="var">Leaf</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">Node</span> <span class="id" type="var">x'</span> <span class="id" type="var">l</span> <span class="id" type="var">r</span> ⇒ <span class="id" type="keyword">if</span> <span class="id" type="var">x</span> &lt;? <span class="id" type="var">x'</span> <span class="id" type="keyword">then</span> <span class="id" type="var">Node</span> <span class="id" type="var">x'</span> (<span class="id" type="var">insertBST'</span> <span class="id" type="var">x</span> <span class="id" type="var">l</span>) <span class="id" type="var">r</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">else</span> <span class="id" type="keyword">if</span> <span class="id" type="var">x'</span> &lt;? <span class="id" type="var">x</span> <span class="id" type="keyword">then</span> <span class="id" type="var">Node</span> <span class="id" type="var">x'</span> <span class="id" type="var">l</span> (<span class="id" type="var">insertBST'</span> <span class="id" type="var">x</span> <span class="id" type="var">r</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">else</span> <span class="id" type="var">t</span><br/>
&nbsp;&nbsp;<span class="id" type="keyword">end</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">insertBST_spec'</span> (<span class="id" type="var">low</span> <span class="id" type="var">high</span> : <span class="id" type="var">nat</span>) (<span class="id" type="var">x</span> : <span class="id" type="var">nat</span>) (<span class="id" type="var">t</span> : <span class="id" type="var">Tree</span> <span class="id" type="var">nat</span>) :=<br/>
&nbsp;&nbsp;(<span class="id" type="var">low</span> &lt;? <span class="id" type="var">x</span>) ==&gt; (<span class="id" type="var">x</span> &lt;? <span class="id" type="var">high</span>) ==&gt; (<span class="id" type="var">isBST</span> <span class="id" type="var">low</span> <span class="id" type="var">high</span> <span class="id" type="var">t</span>) ==&gt; <br/>
&nbsp;&nbsp;<span class="id" type="var">isBST</span> <span class="id" type="var">low</span> <span class="id" type="var">high</span> (<span class="id" type="var">insertBST'</span> <span class="id" type="var">x</span> <span class="id" type="var">t</span>).<br/>
</div>

<div class="doc">
... and try again... 
</div>
<div class="code code-tight">

<span class="comment">(*&nbsp;QuickChick&nbsp;insertBST_spec'.&nbsp;*)</span><br/>
</div>

<div class="doc">
<pre>     ===&gt; 
     QuickChecking insertBST_spec'
     *** Gave up! Passed only 1281 tests
     Discarded: 20000 
</pre>
 ... we see that 90% of tests are being discarded. 
<div class="paragraph"> </div>

<a name="lab73"></a><h4 class="section">练习：4 星, standard (gen_bst)</h4>
 Write a generator that produces binary search trees directly, so
    that you run 10000 tests with 0 discards. 
</div>
<div class="code code-tight">

<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span><br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="code code-tight">

<span class="comment">(*&nbsp;Mon&nbsp;Oct&nbsp;28&nbsp;08:19:01&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
</div>
</div>



</div>

</body>
</html>